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.
---
 ltac/profile_ltac_tactics.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ltac')

diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4
index 0c4e0b0757..ce00c29202 100644
--- a/ltac/profile_ltac_tactics.ml4
+++ b/ltac/profile_ltac_tactics.ml4
@@ -19,7 +19,7 @@ END;;
 
 
 VERNAC COMMAND EXTEND StartProfiling CLASSIFIED AS SIDEFF
- [ "Start" "Profiling" ] -> [ reset_profile(); set_profiling true ]
+ [ "Start" "Profiling" ] -> [ set_profiling true ]
 END
 
 VERNAC COMMAND EXTEND StopProfiling CLASSIFIED AS SIDEFF
-- 
cgit v1.2.3