| changeset 56615 | 47c1dbeec36a |
| parent 56614 | d80f43dab30e |
| child 56631 | 89269bb8e7ca |
--- a/src/Pure/Tools/build.ML Thu Apr 17 11:42:36 2014 +0200 +++ b/src/Pure/Tools/build.ML Thu Apr 17 12:03:15 2014 +0200 @@ -14,7 +14,7 @@ (* command timings *) -type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name * time *) +type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) val empty_timings: timings = Symtab.empty;