# HG changeset patch
# User wenzelm
# Date 1670341328 -3600
# Node ID e5bf43eda6edd2cd99ec3a190192c465daff45ac
# Parent  699d9a219e4509b66a335116cc91222ef930242f
more uniform tooltip for plugin options dialog;

diff -r 699d9a219e45 -r e5bf43eda6ed src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Dec 06 16:38:50 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Dec 06 16:42:08 2022 +0100
@@ -76,7 +76,9 @@
     batches: List[GUI.Selector.Entry[String]]*)
   extends GUI.Selector[String](batches: _*) with JEdit_Options.Entry {
     name = option_name
-    tooltip = Word.capitalize(options.value.description(option_name))
+    tooltip =
+      if (standalone) Word.capitalize(options.value.description(option_name))
+      else options.value.check_name(option_name).print_default
 
     override val title: String =
       options.value.check_name(option_name).title_jedit