From b8d37cdd7541fb898f814e5ca3e6ca0137a5db44 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 22 Feb 2006 14:00:21 +0000 Subject: [PATCH] First part of bug #152 (unable to exit from Matita) solved. --- helm/software/matita/matitaScript.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index b8c950549..d243ebb2e 100644 --- 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 -- 2.39.2