more implicit reload, similar to VSCode;
authorwenzelm
Fri Mar 01 17:00:55 2019 +0100 (7 weeks ago ago)
changeset 7003354243334edcf
parent 70032 29a4f633609e
child 70034 f7c9a1be333f
more implicit reload, similar to VSCode;
src/Tools/jEdit/src/jEdit.props
     1.1 --- a/src/Tools/jEdit/src/jEdit.props	Fri Mar 01 16:49:41 2019 +0100
     1.2 +++ b/src/Tools/jEdit/src/jEdit.props	Fri Mar 01 17:00:55 2019 +0100
     1.3 @@ -1,4 +1,5 @@
     1.4  #jEdit properties
     1.5 +autoReloadDialog=false
     1.6  buffer.deepIndent=false
     1.7  buffer.encoding=UTF-8-Isabelle
     1.8  buffer.indentSize=2