Merge branch 'v8.5' into trunk

1 files changed, 14 insertions, 20 deletions

diff --git a/doc/refman/headers.sty b/doc/refman/headers.sty
index ef28588e3c..fb39f687d7 100644
--- a/doc/refman/headers.sty
+++ b/doc/refman/headers.sty
@@ -30,27 +30,21 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \usepackage{index}
 \makeindex
-\newindex{tactic}{tacidx}{tacind}{%
-\protect\setheaders{Tactics Index}%
-\protect\addcontentsline{toc}{chapter}{Tactics Index}Tactics Index}
 
-\newindex{command}{comidx}{comind}{%
-\protect\setheaders{Vernacular Commands Index}%
-\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}
-
-\renewindex{default}{idx}{ind}{%
-\protect\addcontentsline{toc}{chapter}{Global Index}%
-\protect\setheaders{Global Index}Global Index}
+\newindex{tactic}{tacidx}{tacind}{Tactics Index}
+\newindex{command}{comidx}{comind}{Vernacular Commands Index}
+\newindex{option}{optidx}{optind}{Vernacular Options Index}
+\newindex{error}{erridx}{errind}{Index of Error Messages}
+\renewindex{default}{idx}{ind}{Global Index}
+
+\newcommand{\printrefmanindex}[3]{%
+\cleardoublepage%
+\phantomsection%
+\setheaders{#2}%
+\addcontentsline{toc}{chapter}{#2}%
+\printindex[#1]%
+\cutname{#3}%
+}
 
 \newcommand{\tacindex}[1]{%
 \index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}}