tuned;
authorwenzelm
Thu, 21 May 2015 00:24:02 +0200
changeset 60293 f32c80df1931
parent 60292 ba3c716144dd
child 60294 3841632c7e4f
tuned;
src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed May 20 22:22:27 2015 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Thu May 21 00:24:02 2015 +0200
@@ -1866,8 +1866,7 @@
   \textbf{Workaround:} Use mainstream versions of Linux desktops.
 
   \item \textbf{Problem:} Native Windows look-and-feel with global font
-  scaling leads to bad GUI rendering of various list views, e.g.\ the
-  \emph{Documentation} panel.
+  scaling leads to bad GUI rendering of various tree views.
 
   \textbf{Workaround:} Use \emph{Metal} look-and-feel and re-adjust its
   primary and secondary font as explained in \secref{sec:hdpi}.