aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--test/export/Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/test/export/Makefile b/test/export/Makefile
index d1228bf9..5cad730d 100644
--- a/test/export/Makefile
+++ b/test/export/Makefile
@@ -13,7 +13,7 @@ endif
COQINCLUDES += -R ./clight compcert.test.clight
COQINCLUDES += -R ./csyntax compcert.test.csyntax
-CLIGHTGEN=../../clightgen
+CLIGHTGEN=../../clightgen -stdlib ../../runtime
COQC=coqc
# Regression tests in the current directory