]> matita.cs.unibo.it Git - helm.git/commitdiff
better message
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 28 Jun 2005 17:41:04 +0000 (17:41 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 28 Jun 2005 17:41:04 +0000 (17:41 +0000)
helm/matita/matitacLib.ml

index d00156b8a08c7af834379afaff7a75b14f0eda73..7653427377324b1fe39f45d28347e33f8474adcd 100644 (file)
@@ -78,7 +78,9 @@ let fname () =
 
 let pp_ocaml_mode () = 
   MatitaLog.message "";
-  MatitaLog.message " ** Entering Ocaml mode ** ";
+  MatitaLog.message "                      ** Entering Ocaml mode ** ";
+  MatitaLog.message "";
+  MatitaLog.message "Type 'MatitacLib.go ();;' to enter an interactive matitac";
   MatitaLog.message ""
   
 let rec go () =