diff options
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/extraction/Makefile b/extraction/Makefile index ac162db..0aee0be 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: |