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