diff options
Diffstat (limited to 'doc/manual.tex')
| -rw-r--r-- | doc/manual.tex | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/manual.tex b/doc/manual.tex index d28719a4..d731ecd3 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -67,11 +67,13 @@ \ifdefined\ANON \author{Anonymous} \newcommand\anonymise[1]{\emph{redacted}} +\newcommand\anonymiseomit[1]{} \else \author{Alasdair Armstrong \and Thomas Bauereiss \and Brian Campbell \and Shaked Flur \and Kathryn E. Gray \and Robert Norton-Wright \and Christopher Pulte \and Peter Sewell} \newcommand\anonymise[1]{#1} +\newcommand\anonymiseomit[1]{#1} \fi \maketitle |