aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Timing.ml
Commit message (Expand)AuthorAgeFilesLines
* Removed environment variable for the stdlib_path and added a new variable for...Bernhard Schommer2014-10-061-4/+4
* Moved the timing facility to a seperate file.Bernhard Schommer2014-09-291-0/+63