aboutsummaryrefslogtreecommitdiff
path: root/lib/system.ml
diff options
context:
space:
mode:
authorherbelin2010-06-22 06:28:37 +0000
committerherbelin2010-06-22 06:28:37 +0000
commita1f06f016be512c21cb475491ec9924eea7ff288 (patch)
treeac2a62bef05382047475fdca5cb6a42989772499 /lib/system.ml
parent629048d0bc2a7210eed268ee6484deb2cc11141c (diff)
Protection against anomaly when loading a state with bad magic number.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13175 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/system.ml')
-rw-r--r--lib/system.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/system.ml b/lib/system.ml
index 854c5dbdb0..e0ec7b3ea3 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -255,6 +255,13 @@ let extern_intern ?(warn=true) magic suffix =
in
(extern_state,intern_state)
+let with_magic_number_check f a =
+ try f a
+ with Bad_magic_number fname ->
+ errorlabstrm "with_magic_number_check"
+ (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++
+ strbrk "It is corrupted or was compiled with another version of Coq.")
+
(* Communication through files with another executable *)
let connect writefun readfun com =