]> matita.cs.unibo.it Git - helm.git/commitdiff
missing or rootless dependences now don't break the compilation process
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 18 Mar 2013 21:03:54 +0000 (21:03 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 18 Mar 2013 21:03:54 +0000 (21:03 +0000)
matita/matita/matitaEngine.ml

index 5b9b070bcc105f97ebe98a4be377b937df81ed0c..c1c1cd9078a52cd86c98ea96e4a01ebaa756224b 100644 (file)
@@ -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,_,_ =