1 files changed, 1 insertions, 0 deletions
diff --git a/configure b/configure
index 8261f9f3..dbc53c16 100755
--- a/configure
+++ b/configure
@@ -689,6 +689,7 @@ echo "-R lib compcert.lib \
 -R common compcert.common \
 -R ${arch} compcert.${arch} \
 -R backend compcert.backend \
+-R scheduling compcert.scheduling \
 -R cfrontend compcert.cfrontend \
 -R driver compcert.driver \
 -R flocq compcert.flocq \