]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/library/librarian.ml
components/library: dotdothack removed
[helm.git] / helm / software / components / library / librarian.ml
index f9831545d39fd57ae7ebef2cd539eeec4793f684..919edb36c4f9104eb88ec5be974016b12637533c 100644 (file)
@@ -153,7 +153,6 @@ 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
@@ -357,7 +356,7 @@ module Make = functor (F:Format) -> struct
         make_aux root opts [] [] deps
       else
         make_aux root opts [] [] 
-          (purge_unwanted_roots (List.map F.dotdothack targets) deps)
+          (purge_unwanted_roots targets deps)
     in
     HLog.debug ("Leaving directory '"^root^"'");
     Sys.chdir old_root;