summaryrefslogtreecommitdiff
path: root/extraction/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'extraction/Makefile')
-rw-r--r--extraction/Makefile6
1 files changed, 5 insertions, 1 deletions
diff --git a/extraction/Makefile b/extraction/Makefile
index 5729642..54933cc 100644
--- a/extraction/Makefile
+++ b/extraction/Makefile
@@ -103,7 +103,11 @@ clean::
rm -f ../caml/CMlexer.ml
../caml/Configuration.ml: ../Makefile.config
- echo 'let stdlib_path = "$(LIBDIR)"' > ../caml/Configuration.ml
+ (echo 'let stdlib_path = "$(LIBDIR)"'; \
+ echo 'let prepro = "$(CPREPRO)"'; \
+ echo 'let asm = "$(CASM)"'; \
+ echo 'let linker = "$(CLINKER)"') \
+ > ../caml/Configuration.ml
beforedepend:: ../caml/Configuration.ml
clean::