X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2Flibrarian.ml;h=919edb36c4f9104eb88ec5be974016b12637533c;hb=dfc88cb4e7d0dca81cabe418d2c732cd22166726;hp=f9831545d39fd57ae7ebef2cd539eeec4793f684;hpb=a2257181cddf84a3b831c50398f5b13e2b79ac3a;p=helm.git diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml index f9831545d..919edb36c 100644 --- a/helm/software/components/library/librarian.ml +++ b/helm/software/components/library/librarian.ml @@ -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;