From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 11 Jan 2008 19:11:09 +0000 (+0000)
Subject: added a warning when a file is not compiled cause its buri is readonly
X-Git-Tag: make_still_working~5677
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=85b400c16c933f6ee791f5d2783f466836651a3c;p=helm.git

added a warning when a file is not compiled cause its buri is readonly
---

diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml
index 376c80649..da5136934 100644
--- a/helm/software/components/library/librarian.ml
+++ b/helm/software/components/library/librarian.ml
@@ -300,8 +300,12 @@ module Make = functor (F:Format) -> struct
       let local, remote =
         List.partition (fun (_,_,froot,_) -> froot = Some root) todo
       in
-      let local = List.filter (is_not_ro opts) local in
-       remote @ local
+      let local, skipped = List.partition (is_not_ro opts) local in
+      List.iter 
+       (fun x -> 
+        HLog.warn("Read only baseuri for: "^F.string_of_source_object(fst4 x)))
+       skipped;
+      remote @ local
     in
     if todo <> [] then
       let compiled, failed =