# HG changeset patch
# User wenzelm
# Date 1432160642 -7200
# Node ID f32c80df1931b346583a65cd0451487ca1cbb9e0
# Parent  ba3c716144dd4e30d6111719f0b0a701a6537a95
tuned;

diff -r ba3c716144dd -r f32c80df1931 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}.