aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile7
-rwxr-xr-xconfigure2
2 files changed, 5 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index 3e8324bc0..de4b33edb 100644
--- a/Makefile
+++ b/Makefile
@@ -461,9 +461,9 @@ parsing/g_prim.cmo: parsing/g_prim.ml4
parsing/g_prim.cmx: parsing/g_prim.ml4
$(OCAMLOPT) $(OPTFLAGS) -c -pp "$(CAMLP4EXTEND) -impl" -impl $<
-GRAMMARCMO=./lib/pp_control.cmo ./lib/pp.cmo ./lib/util.cmo ./lib/dyn.cmo \
- ./lib/hashcons.cmo ./parsing/coqast.cmo ./parsing/lexer.cmo \
- ./parsing/pcoq.cmo ./parsing/q_coqast.cmo ./parsing/g_prim.cmo
+GRAMMARCMO=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/dyn.cmo \
+ lib/hashcons.cmo parsing/coqast.cmo parsing/lexer.cmo \
+ parsing/pcoq.cmo parsing/q_coqast.cmo parsing/g_prim.cmo
parsing/grammar.cma: $(GRAMMARCMO)
$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@
@@ -490,6 +490,7 @@ beforedepend:: $(GRAMMARCMO)
parsing/pcoq.ml: parsing/pcoq.ml4
$(CAMLP4EXTEND) pr_o.cmo -impl $< -o $@
+
parsing/extend.ml: parsing/extend.ml4 parsing/grammar.cma
$(CAMLP4GRAMMAR) pr_o.cmo -impl $< -o $@
diff --git a/configure b/configure
index 3c890cf90..c98cf3d2f 100755
--- a/configure
+++ b/configure
@@ -342,7 +342,7 @@ case $ARCH in
win32)
STRIPCOMMAND="true";;
*)
- if test $coq_profile_flag = "-p" ; then
+ if [ "$coq_profile_flag" = "-p" ] ; then
STRIPCOMMAND="true"
else
STRIPCOMMAND="strip"