- no more CSCisms for MathML editor: now use mathml editor debian and

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 2ff1507602b7fcbedfec300026fb3f9c591929f3..1c81ddbbfbc72f6882d67fa5f569c480a87eb9fd 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -455,11 +455,6 @@ let
 
 (* CALLBACKS *)
 
-(*
-ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
- ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
-*)
-
 exception OpenConjecturesStillThere;;
 exception WrongProof;;