From cf07c50b03a49344eb4cbe2e1bc18fcef880b9e9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 12 Feb 2008 12:06:26 +0000
Subject: [PATCH] allow to use "../foo/bar.ma" as a path for the include
 statement

---
 helm/software/components/library/librarian.ml  | 4 +++-
 helm/software/components/library/librarian.mli | 1 +
 helm/software/matita/matitacLib.ml             | 8 ++++++++
 3 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml
index b765f64b6..630cb4425 100644
--- 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 c682579c2..f5698f2f4 100644
--- 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 fc64479f1..80f99ed0d 100644
--- 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) 
-- 
2.39.2