diff options
| author | Jason Gross | 2016-05-14 23:09:20 -0400 |
|---|---|---|
| committer | Jason Gross | 2016-06-05 22:09:40 -0400 |
| commit | 13e11b6aec1444071dc3787da15e89a6bc0eb0dc (patch) | |
| tree | c1e80a141882c806d40a0159be9dbca4be0aa848 /doc | |
| parent | 739ead8b2d70f978e31f793234d7a633636742a1 (diff) | |
Synchronize the profiler state with the document
This is suboptimal, because mutation leaves room for subtle bugs, but
rewriting @tebbi's code to be functional was a pain, and not something I
could figure out how to do easily. I'm working under the assumption
that there is no sharing in a single treenode, which I'm not completely
sure is valid. That said, a few simple tests seem to indicate that this
works as expected.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 24f4b2a775..608793d04f 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1204,7 +1204,7 @@ It is possible to measure the time spent in invocations of primitive tactics as \begin{quote} {\tt Start Profiling}. \end{quote} -Enables the profiler and resets the profile +Enables the profiler \begin{quote} {\tt Stop Profiling}. |