diff options
author | Jason Gross <jgross@mit.edu> | 2018-07-24 19:23:24 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-07-24 19:24:05 -0400 |
commit | ee334b4bff8450afbc580a410fe1225b51260e05 (patch) | |
tree | 89bd6c5549e8adfdd81bda0ddc8bedec66a33273 /extract-function-header.sh | |
parent | 8772868f6b3796d6dd83a76ba2d0525388a71117 (diff) |
User TIMER_FULL for .ml, .hs, compiled files
This gives them different entries in the timing diff
Diffstat (limited to 'extract-function-header.sh')
0 files changed, 0 insertions, 0 deletions