diff options
| author | Jason Gross | 2020-04-29 12:35:58 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-02 13:20:54 -0400 |
| commit | 206e8adedae1b0c479a2cb598510163f909f1a5f (patch) | |
| tree | bce084c1dadd512c2f18659500858abe4c8403e2 /doc/plugin_tutorial | |
| parent | 570dd44feec40ca2be2dd6a4d46ca5378acdce09 (diff) | |
Decrease LtacProf overhead when not profiling
Note that this slightly changes the semantics of backtracking across
`start ltac profiling`.
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions