aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile.build4
-rw-r--r--Makefile.common2
-rw-r--r--config/coq_config.mli1
-rwxr-xr-xconfigure1
-rw-r--r--toplevel/usage.ml2
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
diff --git a/configure b/configure
index edc9b69bb..bbdfe9944 100755
--- a/configure
+++ b/configure
@@ -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 *)