diff options
| author | bertot | 2004-01-22 22:41:55 +0000 |
|---|---|---|
| committer | bertot | 2004-01-22 22:41:55 +0000 |
| commit | 2697e781cb88430859cb0d4a6a8be5f5e4f22c91 (patch) | |
| tree | 54b0bf4aaebc66c1650c081334c4058f18017dff /make.result | |
| parent | d2b4ea2b64cbff52d0f1c19f4c3e7e3caee2f3f1 (diff) | |
change add path commands to get the extra argument and the Hint commands
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5239 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'make.result')
0 files changed, 0 insertions, 0 deletions