Fixed anomaly when trying to load non existing file starting with "./" or "../".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12227 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 2 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 2c63b4cc7..982a607f9 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -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 ->