diff options
Diffstat (limited to 'extraction/Makefile')
-rw-r--r-- | extraction/Makefile | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/extraction/Makefile b/extraction/Makefile index 5729642c..54933cc0 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:: |