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