# HG changeset patch
# User wenzelm
# Date 1464274634 -7200
# Node ID 143f58bb34f956870d790aa4d5fb0ed42024d717
# Parent  c12845e8e80a664611f0b437709c2ff21be183f1
tuned spelling;

diff -r c12845e8e80a -r 143f58bb34f9 NEWS
--- a/NEWS	Thu May 26 15:31:04 2016 +0200
+++ b/NEWS	Thu May 26 16:57:14 2016 +0200
@@ -93,9 +93,9 @@
 
 *** Pure ***
 
-* Code generator: config option "code_timinger" triggers
-measurements of different phases of code generation.  See
-src/HOL/ex/Code_Timing.thy for examples.
+* Code generator: config option "code_timing" triggers measurements of
+different phases of code generation. See src/HOL/ex/Code_Timing.thy for
+examples.
 
 
 *** HOL ***