diff options
| author | gmelquio | 2012-09-16 09:36:41 +0000 |
|---|---|---|
| committer | gmelquio | 2012-09-16 09:36:41 +0000 |
| commit | 636047db18ee199dcc3e6572ea372b8db9664461 (patch) | |
| tree | bca280c49e851b93d07483c11548c48487405393 /plugins/syntax/string_syntax.ml | |
| parent | f4469a308bd007fd70c17b980da753d6e7f070c4 (diff) | |
Fix index generation for the pdf document.
In particular, push all the \tacindex commands outside of the section
titles, as they break index generation when put inside.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15808 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions