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 ***