Matitaweb:

[helm.git] / matitaB / matita / matitaScript.ml

diff --git a/matitaB/matita/matitaScript.ml b/matitaB/matita/matitaScript.ml
index aa51b36a0cc0a3f1f1d6b7a5d17622b2c7d40dfa..6d703b556b3706abeb94281d1c44a0af0dd1d3a4 100644 (file)
--- a/matitaB/matita/matitaScript.ml
+++ b/matitaB/matita/matitaScript.ml
@@ -209,10 +209,10 @@ and eval_statement include_paths (buffer : GText.buffer) status script
           HExtlib.Localized (floc, exn) ->
            HExtlib.raise_localized_exception 
              ~offset:(MatitaGtkMisc.utf8_string_length parsed_text) floc exn
-        | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
+       (* | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
            raise
             (MultiPassDisambiguator.DisambiguationError
-              (offset+parsed_text_length, errorll))
+              (offset+parsed_text_length, errorll)) *)
       in
       assert (text=""); (* no macros inside comments, please! *)
       let st,text = s in