aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-07-28 18:05:39 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-07-28 18:05:39 +0000
commit7e13b8a0627c09a49487dc64210fa4616cffc66c (patch)
treeb44dee28523fd5f63edde51c15571d69251ab221 /toplevel
parent5ce1ece6393b33a213dfba2e3b63a130e398d84f (diff)
Modifications dans les scripts de configuration (coqtop et coqide affichent maintenant le numéro de révision svn) + correction problème OCaml 3.07 et caml_;odify
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9063 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml18
1 files changed, 8 insertions, 10 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0dea6415b..70c85ca4c 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -21,18 +21,16 @@ open Coqinit
let get_version_date () =
try
- let ch = open_in (Coq_config.coqtop^"/make.result") in
- let l = input_line ch in
- let i = String.index l ' ' in
- let j = String.index_from l (i+1) ' ' in
- "checked out on "^(String.sub l (i+1) (j-i-1))
- with _ -> Coq_config.date
+ let ch = open_in (Coq_config.coqtop^"/revision") in
+ let ver = input_line ch in
+ let rev = input_line ch in
+ (ver,rev)
+ with _ -> (Coq_config.version,Coq_config.date)
let print_header () =
- Printf.printf "Welcome to Coq %s (%s)\n"
- Coq_config.version
- (get_version_date ());
- flush stdout
+ let (ver,rev) = (get_version_date ()) in
+ Printf.printf "Welcome to Coq %s (%s)\n" ver rev;
+ flush stdout
let memory_stat = ref false