diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-02-25 23:20:51 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-02-25 23:20:51 +0100 |
| commit | 91284897bbc029cacabc36aae024a86a248814ae (patch) | |
| tree | 09ec6d4ce93d42d978ba5fc0e19e3ac20a1c4ed0 /Makefile | |
| parent | 9e09561f54db459757446db52c01bf3d85bd8764 (diff) | |
| download | compcert-91284897bbc029cacabc36aae024a86a248814ae.tar.gz compcert-91284897bbc029cacabc36aae024a86a248814ae.zip | |
Split up tools and options.
Added additional configuration entries to seperate tools from options in the
.ini files. Internally they are just concatenated in Configuration.ml which
allows it to still use old .ini files.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 5 |
1 files changed, 4 insertions, 1 deletions
@@ -192,8 +192,11 @@ latexdoc: compcert.ini: Makefile.config (echo "stdlib_path=$(LIBDIR)"; \ echo "prepro=$(CPREPRO)"; \ - echo "asm=$(CASM)"; \ echo "linker=$(CLINKER)"; \ + echo "asm=$(CASM)"; \ + echo "prepro_options=$(CPREPRO_OPTIONS)";\ + echo "asm_options=$(CASM_OPTIONS)";\ + echo "linker_options=$(CLINKER_OPTIONS)";\ echo "arch=$(ARCH)"; \ echo "model=$(MODEL)"; \ echo "abi=$(ABI)"; \ |