updated Nitpick documentation to remove weird default for "overlord"
authorblanchet
Fri, 23 Oct 2009 18:57:35 +0200
changeset 331965fe67e108651
parent 33195 0efe26262e73
child 33197 de6285ebcc05
updated Nitpick documentation to remove weird default for "overlord"
doc-src/Nitpick/nitpick.tex
     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}).}