diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-02-17 21:38:13 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-02-17 21:38:13 +0100 |
| commit | 30076f81448721c49b86846de638cbc936c085fb (patch) | |
| tree | caf0b8313f44fdadb5ccbd1b058a8d485fa9d9d5 /doc/refman/headers.sty | |
| parent | 9d141fe86f68f2de7058d317874edc4c0885ebc6 (diff) | |
Separate index for vernacular options.
Diffstat (limited to 'doc/refman/headers.sty')
| -rw-r--r-- | doc/refman/headers.sty | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/refman/headers.sty b/doc/refman/headers.sty index bc5f5c6c3..ef28588e3 100644 --- a/doc/refman/headers.sty +++ b/doc/refman/headers.sty @@ -39,6 +39,11 @@ \protect\addcontentsline{toc}{chapter}{Vernacular Commands Index}% Vernacular Commands Index} +\newindex{option}{optidx}{optind}{% +\protect\setheaders{Vernacular Options Index}% +\protect\addcontentsline{toc}{chapter}{Vernacular Options Index}% +Vernacular Options Index} + \newindex{error}{erridx}{errind}{% \protect\setheaders{Index of Error Messages}% \protect\addcontentsline{toc}{chapter}{Index of Error Messages}Index of Error Messages} @@ -51,6 +56,8 @@ Vernacular Commands Index} \index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}} \newcommand{\comindex}[1]{% \index{#1@\texttt{#1}}\index[command]{#1@\texttt{#1}}} +\newcommand{\optindex}[1]{% +\index{#1@\texttt{#1}}\index[option]{#1@\texttt{#1}}} \newcommand{\errindex}[1]{\texttt{#1}\index[error]{#1}} \newcommand{\errindexbis}[2]{\texttt{#1}\index[error]{#2}} \newcommand{\ttindex}[1]{\index{#1@\texttt{#1}}} |