NEWS
changeset 69775 5a8ae7a4b7d0
parent 69764 3ceff650adb9
child 69778 09ad02c0fbee
--- a/NEWS	Thu Jan 31 16:56:31 2019 +0100
+++ b/NEWS	Thu Jan 31 17:18:15 2019 +0100
@@ -53,6 +53,9 @@
 entries are structured according to chapter / session names, the open
 operation is redirected to the session ROOT file.
 
+* System option "jedit_text_overview" allows to disable the text
+overview column.
+
 * Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
 DejaVu" collection by default, which provides uniform rendering quality
 with the usual Isabelle symbols. Line spacing no longer needs to be