diff options
| author | Pierre-Marie Pédrot | 2015-02-18 17:27:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-18 17:27:39 +0100 |
| commit | 4bb062f4a66c4ae5a1742e7d99fdc335de0d57a9 (patch) | |
| tree | af8ead1cdc5af3842e683f602177ab4fa2dec9b5 /doc/refman/headers.sty | |
| parent | 1be9c4da4d814c29d4ba45b121fda924adc1130e (diff) | |
| parent | 29ba692f0fd25ce87392bbb7494cb62e3b97dc07 (diff) | |
Merge branch 'v8.5'
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 bc5f5c6c3f..ef28588e3c 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}}} |