From a537c9f47ac6be8ecbbef284206869136e43f00b Mon Sep 17 00:00:00 2001
From: glondu
Date: Thu, 17 Sep 2009 17:00:12 +0000
Subject: Replace call to where_in_path by find_file_in_path in "Locate File"

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

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c97c24cd18..7cde4f6378 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -234,12 +234,8 @@ let dump_universes s =
 (* "Locate" commands *)
 
 let locate_file f =
-  try
-    let _,file = System.where_in_path ~warn:false (Library.get_load_paths ()) f in
-    msgnl (str file)
-  with Not_found ->
-    msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++
-		  str"on loadpath"))
+  let _,file = System.find_file_in_path ~warn:false (Library.get_load_paths ()) f in
+  msgnl (str file)
 
 let msg_found_library = function
   | Library.LibLoaded, fulldir, file ->
-- 
cgit v1.2.3