aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2014-12-11 09:29:48 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2014-12-11 09:29:48 +0100
commit866e612bf63568cbe9871bb1d6724323493651e7 (patch)
treeeb8103931a168b91a2e82693a1ab643574b17592 /Makefile
parent2d3330d132b22db7dd44399e0aac6e9e60470f59 (diff)
downloadcompcert-866e612bf63568cbe9871bb1d6724323493651e7.tar.gz
compcert-866e612bf63568cbe9871bb1d6724323493651e7.zip
Preserve single quotes (e.g. in CPREPRO) when generating compcert.ini
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile20
1 files changed, 10 insertions, 10 deletions
diff --git a/Makefile b/Makefile
index 3f87287e..896a456e 100644
--- a/Makefile
+++ b/Makefile
@@ -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