diff --git a/extraction/Makefile b/extraction/Makefile index ac162db78518801a86de66eb1ff626c81c25d36c..0aee0be6f2ac58949be4f3c99b696b9df4552523 100644 --- a/extraction/Makefile +++ b/extraction/Makefile @@ -40,7 +40,8 @@ Configuration.ml: ../Makefile.config echo 'let asm = "$(CASM)"'; \ echo 'let linker = "$(CLINKER)"'; \ echo 'let arch = "$(ARCH)"'; \ - echo 'let variant = "$(VARIANT)"') \ + echo 'let variant = "$(VARIANT)"'; \ + echo 'let system = "$(SYSTEM)"') \ > Configuration.ml clean: