more on GTK;
authorwenzelm
Sat, 23 Nov 2013 12:59:12 +0100
changeset 5529257aefb80b639
parent 55291 bf2519f2bd01
child 55293 83cb91acebcc
more on GTK;
src/Doc/JEdit/JEdit.thy
     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.