diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:17 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:17 +0200 |
commit | 2dad86a4e71bae9905b39970384328316e53eb42 (patch) | |
tree | 9fe7df673a3e36cfbee14f2a4afe5b5b6fc72e80 /lib/system.ml | |
parent | 257f04de91e394cea67254da547fc1b90fa6978d (diff) | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Merge commit 'upstream/8.2pl2+dfsg'
Diffstat (limited to 'lib/system.ml')
-rw-r--r-- | lib/system.ml | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/lib/system.ml b/lib/system.ml index 65826c81..3fa32ef8 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: system.ml 11801 2009-01-18 20:11:41Z herbelin $ *) +(* $Id: system.ml 13175 2010-06-22 06:28:37Z herbelin $ *) open Pp open Util @@ -153,8 +153,12 @@ let where_in_path ?(warn=true) path filename = let find_file_in_path ?(warn=true) paths filename = if not (Filename.is_implicit filename) then - let root = Filename.dirname filename in - root, filename + if Sys.file_exists filename then + let root = Filename.dirname filename in + root, filename + else + errorlabstrm "System.find_file_in_path" + (hov 0 (str "Can't find file" ++ spc () ++ str filename)) else try where_in_path ~warn paths filename with Not_found -> @@ -224,6 +228,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 = |