diff -r 82110cbcf9a1 -r 7a7ad99212b1 NEWS --- a/NEWS Thu Nov 14 11:33:51 2024 +0100 +++ b/NEWS Fri Nov 15 13:08:48 2024 +0100 @@ -140,9 +140,7 @@ C-modifier. * An active highlight area in the input buffer or output panel may be -turned into a text selection by using the ALT modifier. Together with -SHIFT modifier, an existing selection is augmented (otherwise it is -reset). +turned into a text selection by using the ALT modifier. * The "Documentation" panel supports plain text files again, notably "jedit-changes". This was broken in Isabelle2022, Isabelle2023,