diff options
| author | pboutill | 2012-10-15 09:00:16 +0000 |
|---|---|---|
| committer | pboutill | 2012-10-15 09:00:16 +0000 |
| commit | a27c9e7bfe59dba76f1ae7ee139532ce1d4df6f7 (patch) | |
| tree | af5910d5646474c50245e31be695fd67fe856449 /plugins/syntax | |
| parent | 7d4261aebf12e71e12e0224df23c59394e442b39 (diff) | |
Fixing coqdoc index bugs introduced in r14624 and r15053. Revision r14624 introduced bug #2709 on duplicate entries in index and tentative fix of it in r15053 mixed up names of files and names of constants in index (as reported by P. Castéran on coqdev).
Patch by Hugo Herbelin :-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15885 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions