NEWS
changeset 71547 d350aabace23
parent 71545 b0b16088ccf2
child 71551 76ec3baeec9d
--- a/NEWS	Fri Mar 13 16:12:50 2020 +0100
+++ b/NEWS	Fri Mar 13 23:25:34 2020 +0100
@@ -41,7 +41,8 @@
 
 * Mixfix annotations may use "' " (single quote followed by space) to
 separate delimiters (as documented in the isar-ref manual), without
-requiring an auxiliary empty block.
+requiring an auxiliary empty block. A literal single quote needs to be
+escaped properly: rare INCOMPATIBILITY.
 
 
 *** Isar ***