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