diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-12-27 22:32:11 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-12-27 22:42:36 -0500 |
| commit | 1b4bc997554894d4a317eae965f4634e04c11d20 (patch) | |
| tree | 877481391adc92d3da2cab7a5e0e527bdd116ead /configure.ml | |
| parent | 7e319ad03aba413f3165b848eaf821b364f9291b (diff) | |
Add TIMING_SORT_BY and --sort-by to timing scripts
This should help with #5675, in particular with
https://github.com/coq/coq/issues/5675#issuecomment-349716292
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions