From: Michele Galatà <??>
Date: Thu, 29 Aug 2002 13:18:34 +0000 (+0000)
Subject: Comment typo fixed.
X-Git-Tag: new_mathql_before_first_merge~57
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=72c9850370ab0e0b02b3d49a837dd442410f8ba6;p=helm.git

Comment typo fixed.
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 563c88186..bf2918593 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -47,9 +47,9 @@ let htmlfooter =
  "</html>"
 ;;
 
-let prooffile = "/public/sacerdot/currentproof";;
+let prooffile = "/home/galata/miohelm/currentproof";;
 (*CSC: the getter should handle the innertypes, not the FS *)
-let innertypesfile = "/public/sacerdot/innertypes";;
+let innertypesfile = "/home/galata/miohelm/innertypes";;
 
 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
 
@@ -248,7 +248,7 @@ prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent current
 
 (*
 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
- ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ;
+ ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
 *)
 
 let mml_of_cic_term metano term =