From f2320b085559b7470a3dad13cf2a1e9b0c1fb680 Mon Sep 17 00:00:00 2001
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 17 Sep 2009 15:59:03 +0000
Subject: Replace unprotected call to where_in_path by find_file_in_path

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

diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index eb9359107..455e4286a 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -109,7 +109,7 @@ let dir_ml_load s =
 	 * in this file, the Makefile dependency logic needs to be updated.
 	 *)
         let warn = Flags.is_verbose() in
-        let _,gname = where_in_path ~warn !coq_mlpath_copy s in
+        let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in
         try
           Dynlink.loadfile gname;
 	with | Dynlink.Error a ->
-- 
cgit v1.2.3