irediced usage of matita.includes, that is now set by

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

diff --git a/components/library/librarian.ml b/components/library/librarian.ml
index 417035a8138d36a118e2cf0d65bdcc7e05936034..5918136764b6816c5b54dc5a2435d1093fdf02f9 100644 (file)
--- a/components/library/librarian.ml
+++ b/components/library/librarian.ml
@@ -56,7 +56,7 @@ let find_root_for ~include_paths file =
    HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri);
  ensure_trailing_slash root, remove_trailing_slash uri, path
 ;;
-  
+
 let baseuri_of_script ?(include_paths=[]) file = 
   let root, buri, path = find_root_for ~include_paths file in
   let path = HExtlib.normalize_path path in
@@ -75,10 +75,12 @@ let baseuri_of_script ?(include_paths=[]) file =
     try Filename.chop_extension name
     with Invalid_argument "Filename.chop_extension" -> name
   in
+  let extra = String.concat "/" extra_buri in
    root,
    remove_trailing_slash (HExtlib.normalize_path 
-    (buri ^ "/" ^ chop (String.concat "/" extra_buri))),
-   path
+    (buri ^ "/" ^ chop extra)),
+   path,
+   extra
 ;;
 
 let find_roots_in_dir dir =