diff -r 0debd22f0c0e -r 63b18f758874 NEWS
--- a/NEWS	Tue Oct 20 23:53:40 2015 +0200
+++ b/NEWS	Wed Oct 21 00:23:11 2015 +0200
@@ -73,7 +73,8 @@
 * The @{text} antiquotation now ignores the antiquotation option
 "source". The given text content is output unconditionally, without any
 surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the
-argument where they are really intended, e.g. @{text \<open>"foo"\<close>}.
+argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial
+or terminal spaces are ignored.
 
 * HTML presentation uses the standard IsabelleText font and Unicode
 rendering of Isabelle symbols like Isabelle/Scala/jEdit.  The former