diff options
Diffstat (limited to 'doc/refman/headers.hva')
| -rw-r--r-- | doc/refman/headers.hva | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/refman/headers.hva b/doc/refman/headers.hva index f65e1c10c..df4aec272 100644 --- a/doc/refman/headers.hva +++ b/doc/refman/headers.hva @@ -15,6 +15,10 @@ \protect\addcontentsline{toc}{chapter}{Vernacular Commands Index}% Vernacular Commands Index} +\newindex{option}{optidx}{optind}{% +\protect\addcontentsline{toc}{chapter}{Vernacular Options Index}% +Vernacular Options Index} + \newindex{error}{erridx}{errind}{% \protect\addcontentsline{toc}{chapter}{Index of Error Messages}Index of Error Messages} @@ -26,6 +30,8 @@ Global 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}}} |