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} \\
|
