# HG changeset patch
# User wenzelm
# Date 1385207952 -3600
# Node ID 57aefb80b639c59bc85347500b9b2f9ef9cc14c6
# Parent  bf2519f2bd01514a80fb1610240097c43615a158
more on GTK;

diff -r bf2519f2bd01 -r 57aefb80b639 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Fri Nov 22 21:57:50 2013 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sat Nov 23 12:59:12 2013 +0100
@@ -227,7 +227,8 @@
   theme is selected in a Swing-friendly way.\footnote{GTK support in
   Java/Swing was once marketed aggressively by Sun, but never quite
   finished, and is today (2013) lagging a bit behind further
-  development of Swing and GTK.}
+  development of Swing and GTK.  The graphics rendering performance
+  can be worse than for other Swing look-and-feels.}
 
   \item[Windows] Regular \emph{Windows} is used by default, but
   \emph{Windows Classic} also works.