HoTT/HoTT — pull request #348 by JasonGross (2014-03-29 20:31:28+00:00)
Title: Add timing scripts for ammending a commit

I'm going to merge this immediately, since it only touches the `etc/timing` directory.

I use this script to get timings for commits I've already made.