# HG changeset patch
# User blanchet
# Date 1379940823 -7200
# Node ID b6a947a2c615a0b8ba2fe486e651faadb83e3f4e
# Parent  44bc6ff8f350bf8f59faeb02be652ec42fef6480
document "spy"

diff -r 44bc6ff8f350 -r b6a947a2c615 NEWS
--- a/NEWS	Mon Sep 23 14:53:43 2013 +0200
+++ b/NEWS	Mon Sep 23 14:53:43 2013 +0200
@@ -389,6 +389,7 @@
 INCOMPATIBILITY.
 
 * Nitpick:
+  - Added option "spy"
   - Reduce incidence of "too high arity" errors
 
 * Sledgehammer:
diff -r 44bc6ff8f350 -r b6a947a2c615 src/Doc/Nitpick/document/root.tex
--- a/src/Doc/Nitpick/document/root.tex	Mon Sep 23 14:53:43 2013 +0200
+++ b/src/Doc/Nitpick/document/root.tex	Mon Sep 23 14:53:43 2013 +0200
@@ -1951,6 +1951,18 @@
 \nopagebreak
 {\small See also \textit{user\_axioms} (\S\ref{mode-of-operation}).}
 
+\opfalse{spy}{dont\_spy}
+Specifies whether Nitpick should record statistics in
+\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak spy\_\allowbreak nitpick}.
+These statistics can be useful to the developer of Nitpick. If you are willing to have your
+interactions recorded in the name of science, please enable this feature and send the statistics
+file every now and then to the author of this manual (\authoremail).
+To change the default value of this option globally, set the environment variable
+\texttt{NITPICK\_SPY} to \texttt{yes}.
+
+\nopagebreak
+{\small See also \textit{debug} (\S\ref{output-format}).}
+
 \opfalse{overlord}{no\_overlord}
 Specifies whether Nitpick should put its temporary files in
 \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
@@ -2190,7 +2202,8 @@
 option is implicitly disabled for automatic runs.
 
 \nopagebreak
-{\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
+{\small See also \textit{spy} (\S\ref{mode-of-operation}),
+\textit{overlord} (\S\ref{mode-of-operation}), and
 \textit{batch\_size} (\S\ref{optimizations}).}
 
 \opfalse{show\_datatypes}{hide\_datatypes}