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