Package: ppl / 1:1.1-3

latex-header.diff Patch series | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
Index: b/doc/devref-language-interface.tex
===================================================================
--- a/doc/devref-language-interface.tex
+++ b/doc/devref-language-interface.tex
@@ -72,6 +72,8 @@
 
 \setlength{\headheight}{24pt}
 
+\newcommand{\+}{\discretionary{\mbox{\scriptsize$\hookleftarrow$}}{}{}}
+
 \begin{document}
 \title{
 \includegraphics[height=9cm]{ppl_logo.pdf} \\
Index: b/doc/user-language-interface.tex
===================================================================
--- a/doc/user-language-interface.tex
+++ b/doc/user-language-interface.tex
@@ -72,6 +72,8 @@
 
 \setlength{\headheight}{24pt}
 
+\newcommand{\+}{\discretionary{\mbox{\scriptsize$\hookleftarrow$}}{}{}}
+
 \begin{document}
 \title{
 \includegraphics[height=9cm]{ppl_logo.pdf} \\