matita now works reasonably well,

[helm.git] / components / library / librarian.ml

diff --git a/components/library/librarian.ml b/components/library/librarian.ml
index f1649239460939d2915f226bc38b90312df3e82d..72f8c50db9fcfca38e13070a79271e26206bc771 100644 (file)
--- a/components/library/librarian.ml
+++ b/components/library/librarian.ml
@@ -69,9 +69,10 @@ let find_root_for ~include_paths file =
    if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then
      HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri);
    ensure_trailing_slash root, remove_trailing_slash uri, path
- with Failure "find_in" as exn -> 
-   HLog.error ("Unable to find: "^file);
-   raise exn
+ with Failure "find_in" -> 
+   HLog.error ("Unable to find: "^file^"\nPaths explored:\n");
+   List.iter (fun x -> HLog.error (" - "^x^"\n")) include_paths;
+   raise (NoRootFor file)
 ;;
 
 let baseuri_of_script ~include_paths file =