# HG changeset patch
# User wenzelm
# Date 1747747115 -7200
# Node ID 38f5ecbb457496b15059c26f22b57f46f3db438d
# Parent  8d16cafa382ef4cef48c831a8a49b81df5126c68
clarified default properties -- requires to update jedit component;

diff -r 8d16cafa382e -r 38f5ecbb4574 src/Pure/Admin/component_jedit.scala
--- a/src/Pure/Admin/component_jedit.scala	Tue May 20 12:41:53 2025 +0200
+++ b/src/Pure/Admin/component_jedit.scala	Tue May 20 15:18:35 2025 +0200
@@ -453,7 +453,7 @@
 xml-insert-closing-tag.shortcut=
 
 #dark theme
-console.bgColor.dark=\#ff000000
+console.bgColor.dark=\#ff2b2b2b
 console.plainColor.dark=\#ffffffff
 console.caretColor.dark=\#ffffffff
 console.infoColor.dark=\#ffc1dfee