fixed matitamake to handle development with names with spaces

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index f8a9c9bb132a3b23c0596d4b1778a701f06836d0..f7094ab95d282763733ab987af03bd7ec28d94f5 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -147,7 +147,8 @@ let eval_with_engine guistuff status user_goal parsed_text st =
   try
     eval_with_engine guistuff status user_goal parsed_text st
   with
-    MatitaEngine.UnableToInclude what as exc ->
+  | MatitaEngine.UnableToInclude what 
+  | MatitaEngine.IncludedFileNotCompiled what as exc ->
       let compile_needed_and_go_on d =
         let target = what in
         let refresh_cb () =