more uniform color --- avoid odd transparency on Windows (due to jEdit default #666699a);
authorwenzelm
Fri, 11 Sep 2020 12:56:01 +0200
changeset 72253 1b01c626a441
parent 72252 3b17e7688dc6
child 72254 8c5b8d7999bd
child 72257 f2b786884815
more uniform color --- avoid odd transparency on Windows (due to jEdit default #666699a);
src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Fri Sep 11 12:17:19 2020 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Fri Sep 11 12:56:01 2020 +0200
@@ -337,6 +337,7 @@
 view.height=850
 view.middleMousePaste=true
 view.showToolbar=true
+view.status.memory.background=#666699
 view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor java-status ml-status errors clock
 view.thickCaret=true
 view.width=1200