diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-11 14:39:15 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-11 14:39:15 +0000 |
| commit | 25e8fd4c7f0b6d58486c63b32f3a1f4d258a30cb (patch) | |
| tree | 803de7433d4b594aa65f98570ef40a33f2a8506c | |
| parent | fd38a6d8c2e79889d034714dd4b93d6df155aec9 (diff) | |
Fix de divers petits problèmes d'installation
(cherry picked from commit 998a9a62874ba6cf26bdfe28f3ef0c72deaf0c25)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11918 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 4 | ||||
| -rw-r--r-- | Makefile.common | 2 | ||||
| -rw-r--r-- | config/coq_config.mli | 1 | ||||
| -rwxr-xr-x | configure | 1 | ||||
| -rw-r--r-- | toplevel/usage.ml | 2 |
5 files changed, 7 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build index 7b5bd7d51..4175c9a7e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -675,7 +675,7 @@ endif # it with libraries -$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega $(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/contrib/micromega - $(INSTALLLIB) revision $(FULLCOQLIB) + -$(INSTALLLIB) revision $(FULLCOQLIB) install-library-light: $(MKDIR) $(FULLCOQLIB) @@ -684,7 +684,7 @@ install-library-light: $(INSTALLSH) $(FULLCOQLIB) $(INITPLUGINSOPT) $(MKDIR) $(FULLCOQLIB)/states $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states - $(INSTALLLIB) revision $(FULLCOQLIB) + -$(INSTALLLIB) revision $(FULLCOQLIB) install-allreals:: $(INSTALLSH) $(FULLCOQLIB) $(ALLREALS) diff --git a/Makefile.common b/Makefile.common index 1ca51ea5a..7d78d87f9 100644 --- a/Makefile.common +++ b/Makefile.common @@ -899,6 +899,8 @@ COQMLI:=$(KERNELMLI) $(INTERPMLI) $(PRETYPINGMLI) $(TOPLEVELMLI) $(PROOFSMLI) \ # Miscellaneous ########################################################################### +DATE=$(shell LANG=C date +"%B %Y") + SOURCEDOCDIR=dev/source-doc ## Targets forwarded by Makefile to a specific stage diff --git a/config/coq_config.mli b/config/coq_config.mli index 1eff9c38d..b5ccbbca7 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -29,6 +29,7 @@ val coqrunbyteflags : string (* -custom/-dllib -lcoqrun *) (* val defined : string list (* options for lib/ocamlpp *) *) val version : string (* version number of Coq *) +val caml_version : string (* OCaml version used to compile Coq *) val date : string (* release date *) val compile_date : string (* compile date *) val vo_magic_number : int @@ -952,6 +952,7 @@ let arch = "$ARCH" let has_natdynlink = $HASNATDYNLINK let osdeplibs = "$OSDEPLIBS" let version = "$VERSION" +let caml_version = "$CAMLVERSION" let date = "$DATE" let compile_date = "$COMPILEDATE" let vo_magic_number = $VOMAGIC diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 4494a01e9..a9cd00cd4 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -11,7 +11,7 @@ let version () = Printf.printf "The Coq Proof Assistant, version %s (%s)\n" Coq_config.version Coq_config.date; - Printf.printf "compiled on %s\n" Coq_config.compile_date; + Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version; exit 0 (* print the usage of coqtop (or coqc) on channel co *) |