diff options
| author | gmelquio | 2011-04-01 15:14:06 +0000 |
|---|---|---|
| committer | gmelquio | 2011-04-01 15:14:06 +0000 |
| commit | f1bd9d023a01ff064e2d1080a081d7ec178df9a1 (patch) | |
| tree | 4457a7392f21df6f807424b7e3920a1540a7b1d4 /plugins | |
| parent | 6b3f4d6df3366cde21d184b4ada299a66dbf311f (diff) | |
Adjust coqdep so that it behaves like coqtop with respect to the user-contrib directory.
In particular, this directory should be traversed recursively and the full name of its libraries should not be prefixed by the "Coq" logical path.
This fixes coqdep spamming the following message while the yyy library is in the user-contrib loadpath.
*** Warning: in file xxx.v, library yyy.v is required and has not been found in loadpath!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13949 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions