diff options
| author | notin | 2006-10-31 13:43:15 +0000 |
|---|---|---|
| committer | notin | 2006-10-31 13:43:15 +0000 |
| commit | 69c2964cf2a7eb49a83f70947d9ead1ef61f7557 (patch) | |
| tree | 57ecdeebe9a6fe691da94dda826c8cd210fb5f5f /dev/tools | |
| parent | e28561966d4e4a90dd18e00ac6aa76ad5195afd9 (diff) | |
Retour sur la modification apportée en r9289, et nouvelle correction du bug #1259
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9328 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/tools')
0 files changed, 0 insertions, 0 deletions