src/Tools/jEdit/patches/status_bar
changeset 82569 782519a6ebb4
parent 82560 ea65da20d173
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/status_bar	Wed Apr 23 13:32:16 2025 +0200
@@ -0,0 +1,17 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StatusBar.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StatusBar.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StatusBar.java	2024-08-03 19:53:16.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StatusBar.java	2024-11-15 20:22:26.451538237 +0100
+@@ -225,8 +225,11 @@
+ 			else
+ 				this.message.setText(" ");
+ 		}
+-		else
+-			this.message.setText(message);
++		else {
++			Exception exn = new Exception();
++			if (!exn.getStackTrace()[1].getClassName().startsWith("sidekick."))
++				this.message.setText(message);
++		}
+ 	} //}}}
+ 
+ 	//{{{ setMessageComponent() method