1.1 --- a/doc-src/Nitpick/nitpick.tex Fri Oct 23 14:45:01 2009 +0200
1.2 +++ b/doc-src/Nitpick/nitpick.tex Fri Oct 23 18:57:35 2009 +0200
1.3 @@ -1685,9 +1685,7 @@
1.4 Specifies whether Nitpick should put its temporary files in
1.5 \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
1.6 debugging Nitpick but also unsafe if several instances of the tool are run
1.7 -simultaneously. This option is disabled by default unless your home directory
1.8 -ends with \texttt{blanchet} or \texttt{blanchette}.
1.9 -%``I thought there was only one overlord.'' --- Tobias Nipkow
1.10 +simultaneously.
1.11
1.12 \nopagebreak
1.13 {\small See also \textit{debug} (\S\ref{output-format}).}