--- a/src/Tools/jEdit/src/jedit_options.scala Mon Sep 10 19:49:30 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala Mon Sep 10 19:56:08 2012 +0200
@@ -58,7 +58,7 @@
text_area
}
component.load()
- component.tooltip = opt.print
+ component.tooltip = Isabelle.tooltip(opt.print)
component
}
}