diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-17 15:49:22 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-17 15:49:22 +0100 |
commit | 3262e1e2e71b4fad5d5c47603aafb4dcb2539e27 (patch) | |
tree | 4e2d24c2ba129f68da014ea13212a25731d74b9e | |
parent | 4461db2bd92973b83bbd74c8f2eec16d702cffed (diff) | |
download | compcert-3262e1e2e71b4fad5d5c47603aafb4dcb2539e27.tar.gz compcert-3262e1e2e71b4fad5d5c47603aafb4dcb2539e27.zip |
Minor bug fixes in configure and Makefile.extr
-rw-r--r-- | Makefile.extr | 5 | ||||
-rwxr-xr-x | configure | 6 |
2 files changed, 6 insertions, 5 deletions
diff --git a/Makefile.extr b/Makefile.extr index 732df31e..35ae5f7b 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -43,7 +43,7 @@ WARNINGS=-w -3 extraction/%.cmx: WARNINGS +=-w -20 extraction/%.cmo: WARNINGS +=-w -20 -COMPFLAGS=-g $(INCLUDE) $(WARNINGS) +COMPFLAGS=-g $(INCLUDES) $(WARNINGS) # Using the bitstring library and syntax extension (for checklink) @@ -162,6 +162,7 @@ depend: $(GENERATED) @echo "Analyzing OCaml dependencies" @for d in $(DIRS); do $(OCAMLDEP) $$d/*.mli $$d/*.ml; done > .depend.extr ifneq ($(strip $(DIRS_P4)),) - @for d in $(DIRS_P4); do $(OCAMLDEP_P4) $$d/*.mli $$d/*.ml; done >> .dependif + @for d in $(DIRS_P4); do $(OCAMLDEP_P4) $$d/*.mli $$d/*.ml; done >> .depend.extr +endif @@ -213,7 +213,7 @@ fi missingtools=false echo "Testing Coq... " | tr -d '\n' -coq_ver=`(coqc -v | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') 2>/dev/null` +coq_ver=`coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p'` case "$coq_ver" in 8.4pl*) echo "version $coq_ver -- good!";; @@ -253,7 +253,7 @@ else fi echo "Testing Menhir... " | tr -d '\n' -menhir_ver=`(menhir --version | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p') 2>\dev\null` +menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'` case "$menhir_ver" in 201[4-9]*|20[2-9]*) echo "version $menhir_ver -- good!";; @@ -270,7 +270,7 @@ esac echo "Testing GNU make... " | tr -d '\n' make='' for mk in make gmake gnumake; do - make_ver=`($mk -v | head -1 | sed -n -e 's/^GNU Make //p') 2>/dev/null` + make_ver=`($mk -v 2>/dev/null | head -1 | sed -n -e 's/^GNU Make //p') 2>/dev/null` case "$make_ver" in 3.8*|3.9*|[4-9].*) echo "version $make_ver (command '$mk') -- good!" |