From 8031045106d0205136ac1080f0c019961ea4605d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 29 Oct 2002 08:05:04 +0000
Subject: Préservation de la cohérence du cache en cas d'erreur au chargement

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3189 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/library.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/library/library.ml b/library/library.ml
index c7f3ba4330..a653ccc74e 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -362,8 +362,12 @@ let rec intern_library (dir, f) =
 	 pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
          spc() ++ pr_dirpath dir);
     compunit_cache := CompilingModulemap.add dir m !compunit_cache;
-    List.iter (intern_mandatory_library dir) m.library_deps;
-    m
+    try
+      List.iter (intern_mandatory_library dir) m.library_deps;
+      m
+    with e ->
+      compunit_cache := CompilingModulemap.remove dir !compunit_cache; 
+      raise e
 
 and intern_mandatory_library caller (dir,d) =
   let m = intern_absolute_library_from dir in
-- 
cgit v1.2.3