diff options
| author | Jason Gross | 2017-11-17 15:30:14 -0500 |
|---|---|---|
| committer | Jason Gross | 2017-11-17 15:30:14 -0500 |
| commit | 8794dbd18c61109298b827146bcd2b370f5798bd (patch) | |
| tree | 0ed0553493c1eb48dd3cd375ddd7bc5162846770 /tools/TimeFileMaker.py | |
| parent | edf1a8f36f75861b822081b3825357e122b6937d (diff) | |
Have the coq_makefile timing test-suite print more
This should help debug things like
https://github.com/coq/coq/issues/5675#issuecomment-345324924 if they
ever show up again.
Diffstat (limited to 'tools/TimeFileMaker.py')
0 files changed, 0 insertions, 0 deletions