# HG changeset patch
# User wenzelm
# Date 1599821761 -7200
# Node ID 1b01c626a44146ac6b12853d73f79d96d66bd1d0
# Parent  3b17e7688dc6a6f095ec9cd7cb71e7dc2aa594e4
more uniform color --- avoid odd transparency on Windows (due to jEdit default #666699a);

diff -r 3b17e7688dc6 -r 1b01c626a441 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