| changeset 50408 | 1fac4ff86381 |
| parent 50190 | 0d7f0d8fd63b |
| child 50450 | 358b6020f8b6 |
--- a/src/Tools/jEdit/etc/options Thu Dec 06 21:53:35 2012 +0100 +++ b/src/Tools/jEdit/etc/options Thu Dec 06 21:54:43 2012 +0100 @@ -3,9 +3,6 @@ option jedit_logic : string = "" -- "default logic session" -option jedit_auto_start : bool = true - -- "auto-start prover session on editor startup" - option jedit_font_scale : real = 1.0 -- "scale factor of add-on panels wrt. main text area"