# HG changeset patch
# User wenzelm
# Date 1300656403 -3600
# Node ID 7b6e72a1b7dd265b2a36c2aa473c8b1d571e3576
# Parent  75417ef605ba3aa6a02235da2bf256e70a0519b6
NEWS: structure Timing provides various operations for timing;

diff -r 75417ef605ba -r 7b6e72a1b7dd 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.).