diff options
| author | Enrico Tassi | 2016-09-28 16:32:42 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-09-29 10:47:00 +0200 |
| commit | e1df1b77f8c72636b6e347f41f6f38976c86e909 (patch) | |
| tree | fc6fb2a6a6f92a8c7e4a1368855de6f112e95836 /plugins/syntax/string_syntax.ml | |
| parent | ed53e048fc5e4b995c1e0c42bf1ba1611c331cce (diff) | |
-profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100)
With this command line flag one can profile ltac in files
/and/ trim the results without actually touching the files.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions