diff options
| author | Jason Gross | 2016-07-03 17:13:37 -0400 |
|---|---|---|
| committer | Jason Gross | 2016-09-11 19:58:33 -0400 |
| commit | 12cedcbf4dcfe4fd43ab9f4b648314cac26b82db (patch) | |
| tree | e61358df30bef0c7fb145a96ae4a134b645b647f /kernel/type_errors.mli | |
| parent | 74d2ef26ce991c16039db8c06f813836304c6480 (diff) | |
Add support for testing output mod timing changes
Uses sed 's/\s*[0-9]*\.[0-9]\+\s*//g' and 's/\s*0\.\s*//g' to strip
numbers of seconds and to strip percentages. (This can potentially be
extended later.)
Add a test-suite file to make sure that LtacProf outputs some table.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions