diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-11 09:29:48 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-11 09:29:48 +0100 |
commit | 866e612bf63568cbe9871bb1d6724323493651e7 (patch) | |
tree | eb8103931a168b91a2e82693a1ab643574b17592 /Makefile | |
parent | 2d3330d132b22db7dd44399e0aac6e9e60470f59 (diff) | |
download | compcert-866e612bf63568cbe9871bb1d6724323493651e7.tar.gz compcert-866e612bf63568cbe9871bb1d6724323493651e7.zip |
Preserve single quotes (e.g. in CPREPRO) when generating compcert.ini
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 20 |
1 files changed, 10 insertions, 10 deletions
@@ -222,16 +222,16 @@ latexdoc: @chmod -w $*.v compcert.ini: Makefile.config VERSION - (echo stdlib_path=$(LIBDIR); \ - echo prepro=$(CPREPRO); \ - echo asm=$(CASM); \ - echo linker=$(CLINKER); \ - echo arch=$(ARCH); \ - echo model=$(MODEL); \ - echo abi=$(ABI); \ - echo system=$(SYSTEM); \ - echo has_runtime_lib=$(HAS_RUNTIME_LIB); \ - echo asm_supports_cfi=$(ASM_SUPPORTS_CFI); \ + (echo "stdlib_path=$(LIBDIR)"; \ + echo "prepro=$(CPREPRO)"; \ + echo "asm=$(CASM)"; \ + echo "linker=$(CLINKER)"; \ + echo "arch=$(ARCH)"; \ + echo "model=$(MODEL)"; \ + echo "abi=$(ABI)"; \ + echo "system=$(SYSTEM)"; \ + echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \ + echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \ version=`cat VERSION`; \ echo version=$$version) \ > compcert.ini |