fixed matitamake to handle development with names with spaces

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index fe9ea94d66b3ba1dafab5310c035217dcb5f164a..1d23ac063709e3fe57265c86f57a95ae56bcb1e4 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -27,7 +27,8 @@ open Printf
 open MatitaTypes
 
 exception Drop;;
-exception UnableToInclude of string;;
+exception UnableToInclude of string
+exception IncludedFileNotCompiled of string
 
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
@@ -513,8 +514,7 @@ let make_absolute paths path =
   in
   try
     aux paths
-  with Unix.Unix_error _ as exc ->
-    command_error ("File " ^ path ^ " not found")
+  with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
 ;;
        
 let eval_command opts status cmd =
@@ -532,7 +532,8 @@ let eval_command opts status cmd =
      let absolute_path = make_absolute opts.include_paths path in
      let moopath = MatitaMisc.obj_file_of_script absolute_path in
      let ic =
-      try open_in moopath with Sys_error _ -> raise (UnableToInclude moopath) in
+      try open_in moopath with Sys_error _ -> 
+        raise (IncludedFileNotCompiled moopath) in
      let stream = Stream.of_channel ic in
      let status = ref status in
       !eval_from_stream_ref status stream (fun _ _ -> ());