- Fixed the recompilation of config/revision.ml once every two conmpilations.

- Fixed an error message in configure
- Support for filenames with spaces in coqmktop


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11772 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 16 insertions, 17 deletions

diff --git a/Makefile.build b/Makefile.build
index 214095b5f5..908b610623 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -815,21 +815,20 @@ ifeq ($(CHECKEDOUT),git)
 	fi
 endif
 	$(HIDE)set -e; \
-	if test -e revision.new; then \
-          if test -e revision; then \
-	    if test "`cat config/revision.ml`" = "`cat revision.new`" ; then \
-	       rm -f revision.new; \
-            else \
-               mv -f revision.new config/revision.ml; \
-            fi; \
-          else \
-            mv -f revision.new config/revision.ml; \
-          fi; \
-	else \
-	  echo 'let version = Coq_config.version' > config/revision.ml; \
-	  echo 'let revision = Coq_config.date' >> config/revision.ml; \
+	if test ! -e revision.new; then \
+	  echo 'let version = Coq_config.version' > revision.new; \
+	  echo 'let revision = Coq_config.date' >> revision.new; \
 	fi; \
-	echo 'let date = "$(shell date +"%h %d %Y %H:%M:%S")"' >> config/revision.ml
+	echo 'let date = "$(shell date +"%h %d %Y %H:%M:%S")"' >> revision.new ; \
+	if test -e config/revision.ml; then \
+	  if test "`head -2 config/revision.ml`" = "`head -2 revision.new`" ; then \
+	    rm -f revision.new; \
+	  else \
+	    mv -f revision.new config/revision.ml; \
+	  fi; \
+	else \
+	  mv -f revision.new config/revision.ml; \
+	fi
 
 ###########################################################################
 # Default rules
diff --git a/Makefile.common b/Makefile.common
index c679b45e46..0642c5ce25 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -494,7 +494,7 @@ GRAMMARSCMO:=\
   parsing/g_prim.cmo parsing/g_tactic.cmo \
   parsing/g_ltac.cmo parsing/g_constr.cmo
 
-GRAMMARCMO:=$(CONFIG) $(GRAMMARNEEDEDCMO) $(CAMLP4EXTENSIONSCMO) $(GRAMMARSCMO)
+GRAMMARCMO:=config/coq_config.cmo $(GRAMMARNEEDEDCMO) $(CAMLP4EXTENSIONSCMO) $(GRAMMARSCMO)
 
 GRAMMARCMA:=parsing/grammar.cma
 
diff --git a/configure b/configure
index e946f52ddb..76f05e7f32 100755
--- a/configure
+++ b/configure
@@ -474,7 +474,7 @@ else
             elif [ -x "${CAMLLIB}/site-lib/camlp5" ]; then
                 CAMLP4LIB=+site-lib/camlp5
             else
-	        echo "Objective Caml 3.10 found but no Camlp5 installed."
+	        echo "Objective Caml $CAMLVERSION found but no Camlp5 installed."
 	        echo "Configuration script failed!"
 	        exit 1
             fi
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index b765f8620b..f41042807a 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -59,7 +59,7 @@ let includes () =
   let coqlib = Envars.coqlib () in
   let camlp4lib = Envars.camlp4lib () in
     List.fold_right
-      (fun d l -> "-I" :: List.fold_left Filename.concat coqlib d :: l)
+      (fun d l -> "-I" :: ("\"" ^ List.fold_left Filename.concat coqlib d ^ "\"") :: l)
       (src_dirs ())
       (["-I"; "\"" ^ camlp4lib ^ "\""] @ 
 	 ["-I"; "\"" ^ coqlib ^ "\""] @