From 7534c1c085b2bd066f44d87c3caeb317e93d224c Mon Sep 17 00:00:00 2001
From: notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 7 Jan 2009 14:58:35 +0000
Subject: Suite de la révision #11756
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11757 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile             |  2 +-
 Makefile.build       | 14 +++++++-------
 Makefile.common      | 13 +++++--------
 tools/coqdoc/main.ml |  2 +-
 4 files changed, 14 insertions(+), 17 deletions(-)

diff --git a/Makefile b/Makefile
index 9d23feeb4..3aa0be729 100644
--- a/Makefile
+++ b/Makefile
@@ -208,7 +208,7 @@ depclean:
 	find . $(FIND_VCS_CLAUSE) -name '*.d' | xargs rm -f
 
 cleanconfig:
-	rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli $(REVISIONML)
+	rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli config/revision.ml
 
 distclean: clean cleanconfig
 
diff --git a/Makefile.build b/Makefile.build
index 1afa656a9..908213d42 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -784,7 +784,7 @@ $(foreach f,$(RECTYPESML),$(eval $(call rectypes-rules-template,$(f))))
 # source tree
 .PHONY: revision
 
-revision $(REVISIONML):
+revision config/revision.ml:
 	$(SHOW)'CHECK revision'
 	$(HIDE)rm -f revision.new
 ifeq ($(CHECKEDOUT),svn)
@@ -817,19 +817,19 @@ endif
 	$(HIDE)set -e; \
 	if test -e revision.new; then \
           if test -e revision; then \
-	    if test "`cat $(REVISIONML)`" = "`cat revision.new`" ; then \
+	    if test "`cat config/revision.ml`" = "`cat revision.new`" ; then \
 	       rm -f revision.new; \
             else \
-               mv -f revision.new $(REVISIONML); \
+               mv -f revision.new config/revision.ml; \
             fi; \
           else \
-            mv -f revision.new $(REVISIONML); \
+            mv -f revision.new config/revision.ml; \
           fi; \
 	else \
-	  echo 'let version = Coq_config.version' > $(REVISIONML); \
-	  echo 'let revision = Coq_config.date' >> $(REVISIONML); \
+	  echo 'let version = Coq_config.version' > config/revision.ml; \
+	  echo 'let revision = Coq_config.date' >> config/revision.ml; \
 	fi; \
-	echo 'let date = "$(shell date +"%h %d %Y %H:%M:%S")"' >> $(REVISIONML)
+	echo 'let date = "$(shell date +"%h %d %Y %H:%M:%S")"' >> config/revision.ml
 
 ###########################################################################
 # Default rules
diff --git a/Makefile.common b/Makefile.common
index 9c1962af7..f2c02d48e 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -126,10 +126,7 @@ CLIBS:=unix.cma
 CAMLP4OBJS:=gramlib.cma
 
 CONFIG:=\
-  config/coq_config.cmo
-
-REVISIONML:=config/revision.ml
-REVISIONCMO:=$(REVISIONML:.ml=.cmo)
+  config/coq_config.cmo config/revision.cmo
 
 LIBREP:=\
   lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \
@@ -230,7 +227,7 @@ TOPLEVEL:=\
   toplevel/vernacinterp.cmo toplevel/mltop.cmo \
   toplevel/vernacentries.cmo toplevel/whelp.cmo toplevel/vernac.cmo \
   toplevel/line_oriented_parser.cmo toplevel/protectedtoplevel.cmo \
-  toplevel/toplevel.cmo $(REVISIONCMO) toplevel/usage.cmo \
+  toplevel/toplevel.cmo toplevel/usage.cmo \
   toplevel/coqinit.cmo toplevel/coqtop.cmo
 
 HIGHTACTICS:=\
@@ -394,7 +391,7 @@ COQENVCMO:=$(CONFIG) lib/pp_control.cmo lib/pp.cmo  lib/compat.cmo lib/flags.cmo
 COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo 
 COQMKTOPCMX:=$(COQMKTOPCMO:.cmo=.cmx)
 
-COQCCMO:=$(COQENVCMO) $(REVISIONCMO) toplevel/usage.cmo scripts/coqc.cmo
+COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo
 COQCCMX:=$(COQCCMO:.cmo=.cmx)
 
 INTERFACE:=\
@@ -443,7 +440,7 @@ COQDOCCMO:=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \
 # checker
 
 MCHECKER:=\
-  config/coq_config.cmo $(REVISIONCMO) \
+  $(CONFIG) \
   lib/pp_control.cmo lib/pp.cmo lib/compat.cmo \
   lib/flags.cmo lib/util.cmo lib/option.cmo lib/hashcons.cmo \
   lib/system.cmo lib/envars.cmo \
@@ -512,7 +509,7 @@ STAGE1_CMO:=$(GRAMMARCMO) parsing/q_constr.cmo
 STAGE1:=parsing/grammar.cma parsing/q_constr.cmo
 
 PRINTERSCMO:=\
-  config/coq_config.cmo lib/lib.cma \
+  $(CONFIG) lib/lib.cma \
   kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo kernel/term.cmo	\
   kernel/mod_subst.cmo kernel/copcodes.cmo kernel/cemitcodes.cmo	\
   kernel/sign.cmo kernel/declarations.cmo kernel/retroknowledge.cmo \
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 864b2718e..65e2045a1 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -78,7 +78,7 @@ let obsolete s =
 
 let banner () =
   eprintf "This is coqdoc version %s, compiled on %s\n"
-    Coq_config.version Coq_config.compile_date;
+    Revision.version Revision.date;
   flush stderr
     
 let target_full_name f = 
-- 
cgit v1.2.3