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