diff options
author | 2016-09-28 16:32:42 +0200 | |
---|---|---|
committer | 2016-09-29 10:47:00 +0200 | |
commit | e1df1b77f8c72636b6e347f41f6f38976c86e909 (patch) | |
tree | fc6fb2a6a6f92a8c7e4a1368855de6f112e95836 /test-suite/output/Arguments.v | |
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 'test-suite/output/Arguments.v')
0 files changed, 0 insertions, 0 deletions