matitac now compiles like make (recorsively) if needed.

[helm.git] / matita / matitaExcPp.ml

diff --git a/matita/matitaExcPp.ml b/matita/matitaExcPp.ml
index 8888b8dfed312db253a8d2c31b3b11a58b963d7d..14e7a0db8777adcea5f59fa871c9fc725ba04222 100644 (file)
--- a/matita/matitaExcPp.ml
+++ b/matita/matitaExcPp.ml
@@ -117,10 +117,6 @@ let rec to_string =
       let _,msg = to_string exn in
       let (x, y) = HExtlib.loc_of_floc floc in
        Some floc, sprintf "Error at %d-%d: %s" x y msg
-  | GrafiteTypes.Option_error ("baseuri", "not found" ) -> 
-      None,
-      "Baseuri not set for this script. "
-      ^ "Use 'set \"baseuri\" \"<uri>\".' to set it."
   | GrafiteTypes.Command_error msg -> None, "Error: " ^ msg
   | CicNotationParser.Parse_error err ->
       None, sprintf "Parse error: %s" err