First part of bug #152 (unable to exit from Matita) solved.

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index b8c9505497305dcc0f407d2ae8f448d0c29120e6..d243ebb2ead2ad2c5f65708646cf25c02137e363 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -803,6 +803,7 @@ object (self)
     try
       is_there_only_comments self#lexicon_status s
     with 
+    | HExtlib.Localized _
     | CicNotationParser.Parse_error _ -> false
     | Margin | End_of_file -> true