# HG changeset patch
# User blanchet
# Date 1379940823 -7200
# Node ID 342e371395c66324ed9375b8a926809becca3c98
# Parent  ac1ec50653164b62073edf1ab67ed0793e819d1a
document "spy" option

diff -r ac1ec5065316 -r 342e371395c6 NEWS
--- a/NEWS	Mon Sep 23 14:53:43 2013 +0200
+++ b/NEWS	Mon Sep 23 14:53:43 2013 +0200
@@ -395,7 +395,7 @@
   - Renamed option:
       isar_shrink ~> isar_compress
     INCOMPATIBILITY.
-  - Added option "isar_try0"
+  - Added options "isar_try0", "spy"
   - Better support for "isar_proofs"
   - MaSh has been fined-tuned and now runs as a local server
 
diff -r ac1ec5065316 -r 342e371395c6 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Mon Sep 23 14:53:43 2013 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Sep 23 14:53:43 2013 +0200
@@ -1016,6 +1016,18 @@
 {\small See also \textit{preplay\_timeout} (\S\ref{timeouts})
 and \textit{dont\_preplay} (\S\ref{timeouts}).}
 
+\opfalse{spy}{dont\_spy}
+Specifies whether Sledgehammer should record statistics in
+\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak spy\_\allowbreak sledgehammer}.
+These statistics can be useful to the developers of Sledgehammer. 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{SLEDGEHAMMER\_SPY} to \texttt{yes}.
+
+\nopagebreak
+{\small See also \textit{debug} (\S\ref{output-format}).}
+
 \opfalse{overlord}{no\_overlord}
 Specifies whether Sledgehammer should put its temporary files in
 \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
@@ -1280,7 +1292,8 @@
 automatic runs.
 
 \nopagebreak
-{\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
+{\small See also \textit{spy} (\S\ref{mode-of-operation}) and
+\textit{overlord} (\S\ref{mode-of-operation}).}
 
 \opsmart{isar\_proofs}{no\_isar\_proofs}
 Specifies whether Isar proofs should be output in addition to one-liner