From 13e11b6aec1444071dc3787da15e89a6bc0eb0dc Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 14 May 2016 23:09:20 -0400
Subject: 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.
---
 doc/refman/RefMan-ltac.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

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}.
-- 
cgit v1.2.3