src/Tools/jEdit/patches/status_bar
author wenzelm
Wed, 23 Apr 2025 13:32:16 +0200
changeset 82569 782519a6ebb4
parent 82560 src/Tools/jEdit/patches/menus_and_sidekick@ea65da20d173
permissions -rw-r--r--
clarified patches;

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