allow to use "../foo/bar.ma" as a path for the include statement

diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml
index b765f64b65c37b4c4607ce66db06d5dd4c8e7524..630cb44258eb2f6593039dfbf7cea0dd11fa4687 100644 (file)
--- a/helm/software/components/library/librarian.ml
+++ b/helm/software/components/library/librarian.ml
@@ -153,6 +153,7 @@ module type Format =
     val mtime_of_source_object: source_object -> float option
     val mtime_of_target_object: target_object -> float option
     val is_readonly_buri_of: options -> source_object -> bool
+    val dotdothack: source_object -> source_object 
   end
 
 module Make = functor (F:Format) -> struct
@@ -355,7 +356,8 @@ module Make = functor (F:Format) -> struct
       if targets = [] then 
         make_aux root opts [] [] deps
       else
-        make_aux root opts [] [] (purge_unwanted_roots targets deps)
+        make_aux root opts [] [] 
+          (purge_unwanted_roots (List.map F.dotdothack targets) deps)
     in
     HLog.debug ("Leaving directory '"^root^"'");
     Sys.chdir old_root;

diff --git a/helm/software/components/library/librarian.mli b/helm/software/components/library/librarian.mli
index c682579c2352845cb4886cf87d462a6d291a94e7..f5698f2f476f03725e08c6c3767b9d3539b5f31c 100644 (file)
--- a/helm/software/components/library/librarian.mli
+++ b/helm/software/components/library/librarian.mli
@@ -74,6 +74,7 @@ module type Format =
     val mtime_of_source_object: source_object -> float option
     val mtime_of_target_object: target_object -> float option
     val is_readonly_buri_of: options -> source_object -> bool
+    val dotdothack: source_object -> source_object 
   end
 
 module Make :

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index fc64479f12fd8fce2e896a628028cf7c9a597b05..80f99ed0de685508e0c50411fff6b0de64f0e173 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -308,6 +308,14 @@ module F =
 
     let load_deps_file = Librarian.load_deps_file;;
 
+    let dotdothack s = 
+      let rec aux = function
+        | ".." :: _ :: tl -> aux tl
+        | x -> x
+      in
+      String.concat "/" (aux (Str.split (Str.regexp "/") s))
+    ;;
+
   end 
 
 module Make = Librarian.Make(F)