From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 29 Sep 2008 16:40:48 +0000 (+0000)
Subject: quick fix to make read-only baseuri non compiled but considered successful
X-Git-Tag: make_still_working~4723
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2ce98fa7862b4cb93f7e62d1474092bece17c1d0;p=helm.git

quick fix to make read-only baseuri non compiled but considered successful
---

diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml
index 6cedc0101..4c222b0b9 100644
--- a/helm/software/components/library/librarian.ml
+++ b/helm/software/components/library/librarian.ml
@@ -420,7 +420,10 @@ module Make = functor (F:Format) -> struct
 		   let res = F.build lo t in
 		   time_stamp ("L : DONE     " ^ str); res
 		end else begin
-		   HLog.warn("Read only baseuri for: "^ str); false
+                   Hashtbl.remove ct tgt;
+                   Hashtbl.add ct tgt None;
+		   HLog.warn("Read only baseuri for: "^ str^
+                     ", assuming it is aleary built."); true
 		end
              | Some froot -> make froot [t]
              | None ->