src/Tools/jEdit/etc/options
changeset 54881 dff57132cf18
parent 54377 750561986828
child 55033 8e8243975860
--- a/src/Tools/jEdit/etc/options	Mon Dec 30 12:58:13 2013 +0100
+++ b/src/Tools/jEdit/etc/options	Mon Dec 30 20:35:17 2013 +0100
@@ -3,6 +3,9 @@
 public option jedit_logic : string = ""
   -- "default logic session"
 
+public option jedit_print_mode : string = ""
+  -- "default print modes for output, separated by commas (change requires restart)"
+
 public option jedit_auto_load : bool = false
   -- "load all required files automatically to resolve theory imports"