diff options
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}. |