aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.ml
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-02-11 14:39:08 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-02-11 14:39:08 +0000
commitf930602d29ee71144b620629b3f7148e22e309c1 (patch)
tree4baacee4b4b3d3d01d55d8820e46b353a05ffcc2 /ide/coq.ml
parentf4c9a46f34ff775f6e19a1f93e2a8d408cf9f3ad (diff)
Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11915 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.ml')
-rw-r--r--ide/coq.ml22
1 files changed, 16 insertions, 6 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index e58a1bd19..c6aad9ffa 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -52,21 +52,31 @@ let init () =
let i = ref 0
-let short_version () =
- let revision =
- if Glib.Utf8.validate Revision.revision
- then Revision.revision
+let get_version_date () =
+ let date =
+ if Glib.Utf8.validate Coq_config.date
+ then Coq_config.date
else "<date not printable>" in
- Printf.sprintf "The Coq Proof Assistant, version %s (%s)\n" Revision.version revision
+ try
+ let ch = open_in (Coq_config.coqsrc^"/revision") in
+ let ver = input_line ch in
+ let rev = input_line ch in
+ (ver,rev)
+ with _ -> (Coq_config.version,date)
+
+let short_version () =
+ let (ver,date) = get_version_date () in
+ Printf.sprintf "The Coq Proof Assistant, version %s (%s)\n" ver date
let version () =
+ let (ver,date) = get_version_date () in
Printf.sprintf
"The Coq Proof Assistant, version %s (%s)\
\nArchitecture %s running %s operating system\
\nGtk version is %s\
\nThis is the %s version (%s is the best one for this architecture and OS)\
\n"
- Revision.version Revision.revision
+ ver date
Coq_config.arch Sys.os_type
(let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
(if Mltop.is_native then "native" else "bytecode")