From 9aecb4427f0f8ca3cb4c26bc7f73bb74164a93d9 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 13 Mar 2013 00:00:17 +0000
Subject: Restrict (try...with...) to avoid catching critical exn (part 8)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/nativelib.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativelib.ml')

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 46125a2c7..6b2b4aa7c 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -91,7 +91,7 @@ let call_linker ~fatal prefix f upds =
    with | Dynlink.Error e ->
           let msg = "Dynlink error, " ^ Dynlink.error_message e in
           if fatal then anomaly (Pp.str msg) else Pp.msg_warning (Pp.str msg)
-        | _ ->
+        | e when Errors.noncritical e ->
           let msg = "Dynlink error" in
           if fatal then anomaly (Pp.str msg) else Pp.msg_warning (Pp.str msg));
   match upds with Some upds -> update_locations upds | _ -> ()
-- 
cgit v1.2.3