author | wenzelm |
Thu, 17 Apr 2014 12:03:15 +0200 | |
changeset 56615 | 47c1dbeec36a |
parent 56614 | d80f43dab30e |
child 56616 | abc2da18d08d |
--- 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;