# HG changeset patch
# User wenzelm
# Date 1397728995 -7200
# Node ID 47c1dbeec36a17fc96cdf5af08a890dea7a5c112
# Parent  d80f43dab30e7f3c5b69c8b7689a6fed1a4ce953
tuned comments;

diff -r d80f43dab30e -r 47c1dbeec36a 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;