From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 18 Mar 2013 21:03:54 +0000 (+0000)
Subject: missing or rootless dependences now don't break the compilation process
X-Git-Tag: make_still_working~1204
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aa05f446eeddaecd257c5176b7f0199e34284ac0;p=helm.git

missing or rootless dependences now don't break the compilation process
---

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 5b9b070bc..c1c1cd907 100644
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -360,10 +360,13 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
         let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
         let asserted,children_bad =
          List.fold_left
-          (fun (asserted,b) mapath ->
-            let asserted,b1 =
-              assert_ng ~already_included ~compiling ~asserted ~include_paths
-               mapath
+          (fun (asserted,b) mapath -> 
+	    let asserted,b1 =
+              try 
+	       assert_ng ~already_included ~compiling ~asserted ~include_paths
+                mapath
+	      with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
+	        asserted, true 
             in
              asserted, b || b1
               || let _,baseuri,_,_ =