src/Tools/jEdit/etc/options

--- a/src/Tools/jEdit/etc/options	Fri Apr 05 23:45:35 2019 +0200
+++ b/src/Tools/jEdit/etc/options	Sat Apr 06 22:05:25 2019 +0200
@@ -39,6 +39,9 @@
 public option jedit_text_overview : bool = true
   -- "paint text overview column"
 
+public option isabelle_fonts_hinted : bool = true
+  -- "use hinted Isabelle DejaVu fonts (change requires restart)"
+
 
 section "Indentation"