diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/profile_ltac_tactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
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 |