changeset 71551 | 76ec3baeec9d |
parent 71547 | d350aabace23 |
child 71557 | 61ba52af28e3 |
child 71575 | aff37005fd79 |
--- a/NEWS Sat Mar 14 13:49:52 2020 +0100 +++ b/NEWS Sat Mar 14 14:23:52 2020 +0100 @@ -42,7 +42,7 @@ * 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. A literal single quote needs to be -escaped properly: rare INCOMPATIBILITY. +escaped properly. Minor INCOMPATIBILITY. *** Isar ***