# HG changeset patch
# User wenzelm
# Date 1551456055 -3600
# Node ID 54243334edcf75825c11e5728aa479b7d0bdd1cd
# Parent  29a4f633609e4fa429b3bc46941f4d7751046ee6
more implicit reload, similar to VSCode;

diff -r 29a4f633609e -r 54243334edcf src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Fri Mar 01 16:49:41 2019 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Fri Mar 01 17:00:55 2019 +0100
@@ -1,4 +1,5 @@
 #jEdit properties
+autoReloadDialog=false
 buffer.deepIndent=false
 buffer.encoding=UTF-8-Isabelle
 buffer.indentSize=2