aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml15
1 files changed, 1 insertions, 14 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9ada5bff2..b4e23a874 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -19,19 +19,6 @@ open States
open Toplevel
open Coqinit
-let get_version_date () =
- 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,Coq_config.date)
-
-let print_header () =
- let (ver,rev) = (get_version_date ()) in
- Printf.printf "Welcome to Coq %s (%s)\n" ver rev;
- flush stdout
-
let output_context = ref false
let memory_stat = ref false
@@ -337,7 +324,7 @@ let init is_ide =
try
parse_args is_ide;
re_exec is_ide;
- if_verbose print_header ();
+ if_verbose Usage.print_header ();
init_load_path ();
inputstate ();
set_vm_opt ();