Extracted addition to texinfo.tex (for @doubleleftarrow{} command) into

supplemental file texinfo-suppl.tex.  This file must be input *before*
texinfo.tex, as is done in admin.texinfo and install.texinfo.

git-svn-id: svn://anonsvn.mit.edu/krb5/trunk@9065 dc483132-0cff-0310-8789-dd5450dbe970

diff --git a/doc/admin.texinfo b/doc/admin.texinfo
index 04730717fc936838030ca8b08ed2e5d9ca0f8ae3..fcff1ccac758697179fdf3cdbea6a27e3ba2c6c6 100644 (file)
--- a/doc/admin.texinfo
+++ b/doc/admin.texinfo
@@ -1,6 +1,6 @@
+\input texinfo-suppl.tex        % contains @doubleleftarrow{} definition
+                                % this line must come *before* \input texinfo
 \input texinfo @c -*-texinfo-*-
-@c Note: the above texinfo file must include the "doubleleftarrow"
-@c definitions added by jcb.
 @c %**start of header
 @c guide
 @setfilename kerberos-admin.info

diff --git a/doc/install.texinfo b/doc/install.texinfo
index 7e2f15fbf32ef61b23a0d7735f9a96588c878af4..f8307c73cd9d087bddb301aeab8843b9d8f911eb 100644 (file)
--- a/doc/install.texinfo
+++ b/doc/install.texinfo
@@ -1,7 +1,6 @@
+\input texinfo-suppl.tex        % contains @doubleleftarrow{} definition
+                                % this line must come *before* \input texinfo
 \input texinfo @c -*-texinfo-*-
-@c
-@c Note: the above texinfo file must include the "doubleleftarrow"
-@c definitions added by jcb.
 @c %**start of header
 @c guide
 @setfilename krb5-install.info

diff --git a/doc/texinfo-suppl.tex b/doc/texinfo-suppl.tex
new file mode 100644 (file)
index 0000000..4a1c0cd
--- /dev/null
+++ b/doc/texinfo-suppl.tex
@@ -0,0 +1,7 @@
+\def\temp{
+\chapternofonts
+\def\doubleleftarrow{\realbackslash doubleleftarrow}
+}
+\let\chapternofonts=\temp
+
+\def\doubleleftarrow{\leavevmode\raise.15ex\hbox to 1em{\hfil$\Leftarrow$\hfil}}

diff --git a/doc/texinfo.tex b/doc/texinfo.tex
index 991508d547ce662cdecfe413a4024cd447265369..9d4147edcaec75096ebd6a3f44d80b980ba3a3f3 100644 (file)
--- a/doc/texinfo.tex
+++ b/doc/texinfo.tex
@@ -2353,7 +2353,6 @@ July\or August\or September\or October\or November\or December\fi
 \let\rawbackslash=\relax%
 \let\frenchspacing=\relax%
 \def\result{\realbackslash result}
-\def\doubleleftarrow{\realbackslash doubleleftarrow}
 \def\equiv{\realbackslash equiv}
 \def\expansion{\realbackslash expansion}
 \def\print{\realbackslash print}
@@ -2361,7 +2360,7 @@ July\or August\or September\or October\or November\or December\fi
 \def\dots{\realbackslash dots}
 \def\copyright{\realbackslash copyright}
 \def\tt{\realbackslash tt}
-\def\bf{\realbackslash bf }
+\def\bf{\realbackslash bf}
 \def\w{\realbackslash w}
 \def\less{\realbackslash less}
 \def\gtr{\realbackslash gtr}
@@ -3012,7 +3011,6 @@ July\or August\or September\or October\or November\or December\fi
 \def\point{$\star$}
 
 \def\result{\leavevmode\raise.15ex\hbox to 1em{\hfil$\Rightarrow$\hfil}}
-\def\doubleleftarrow{\leavevmode\raise.15ex\hbox to 1em{\hfil$\Leftarrow$\hfil}}
 \def\expansion{\leavevmode\raise.1ex\hbox to 1em{\hfil$\mapsto$\hfil}}
 \def\print{\leavevmode\lower.1ex\hbox to 1em{\hfil$\dashv$\hfil}}