tuned comments;
authorwenzelm
Thu Apr 17 12:03:15 2014 +0200 (2014-04-17)
changeset 5661547c1dbeec36a
parent 56614 d80f43dab30e
child 56616 abc2da18d08d
tuned comments;
src/Pure/Tools/build.ML
     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