From 30076f81448721c49b86846de638cbc936c085fb Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 17 Feb 2015 21:38:13 +0100
Subject: Separate index for vernacular options.

---
 doc/refman/headers.sty | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'doc/refman/headers.sty')

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}}}
-- 
cgit v1.2.3