NEWS: structure Timing provides various operations for timing;
authorwenzelm
Sun, 20 Mar 2011 22:26:43 +0100
changeset 42015 7b6e72a1b7dd
parent 42014 75417ef605ba
child 42016 3b6826b3ed37
NEWS: structure Timing provides various operations for timing;
NEWS
--- a/NEWS	Sun Mar 20 22:08:12 2011 +0100
+++ b/NEWS	Sun Mar 20 22:26:43 2011 +0100
@@ -65,6 +65,9 @@
 
 *** ML ***
 
+* Structure Timing provides various operations for timing; supersedes
+former start_timing/end_timing etc.
+
 * Path.print is the official way to show file-system paths to users
 (including quotes etc.).