aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-14 18:47:34 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-14 18:47:34 +0000
commit3f787586c709a75e73837e4384d10752079bc646 (patch)
treec366a9045ce4f8d904c68767647a95db984e3a81 /tools
parenta0717999ef44b284fd761ee86bf5f2c25feccba0 (diff)
Reorder search path order, so the standard library is search last.
This allows the construction of an extended library that shadows the standard library. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14000 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdep.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index e9226d383..ccce7cd31 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -190,6 +190,7 @@ let coqdep () =
if Array.length Sys.argv < 2 then usage ();
parse (List.tl (Array.to_list Sys.argv));
if not Coq_config.has_natdynlink then option_natdynlk := false;
+ (* NOTE: These directories are searched from last to first *)
if !Flags.boot then begin
add_rec_dir add_known "theories" ["Coq"];
add_rec_dir add_known "plugins" ["Coq"]