# HG changeset patch
# User wenzelm
# Date 1548703929 -3600
# Node ID 2755c387f1e680146af6b964334bf7446797baa0
# Parent  7404f5b91e56710848ff483d520e84116ac55031
revert accident with raw Unicode (not Isabelle symbols) in 7404f5b91e56;

diff -r 7404f5b91e56 -r 2755c387f1e6 NEWS
--- a/NEWS	Mon Jan 28 16:29:11 2019 +0100
+++ b/NEWS	Mon Jan 28 20:32:09 2019 +0100
@@ -3002,9 +3002,9 @@
 performance.
 
 * Property values in etc/symbols may contain spaces, if written with the
-replacement character "?" (Unicode point 0x2324). For example:
-
-    \<star>  code: 0x0022c6  group: operator  font: Deja?Vu?Sans?Mono
+replacement character "␣" (Unicode point 0x2324). For example:
+
+    \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono
 
 * Java runtime environment for x86_64-windows allows to use larger heap
 space.