# HG changeset patch
# User blanchet
# Date 1256317055 -7200
# Node ID 5fe67e108651e1222f6218126d014dec6e2fa574
# Parent  0efe26262e7315e1778959212c5a4637738415d9
updated Nitpick documentation to remove weird default for "overlord"

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