# HG changeset patch
# User wenzelm
# Date 1432300235 -7200
# Node ID 9e8d0f8e552b46b592ae90cf1b4be93b078eef99
# Parent  3f0bb5c58dfab8e436c50d5ee3983c30eac527fc
tuned;

diff -r 3f0bb5c58dfa -r 9e8d0f8e552b src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Thu May 21 14:03:17 2015 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Fri May 22 15:10:35 2015 +0200
@@ -315,7 +315,7 @@
   in mind that this extra variance of GUI functionality is unlikely to
   work in arbitrary combinations.  The platform-independent
   \emph{Nimbus} and \emph{Metal} should always work.  The historic
-  \emph{CDE/Motif} is better ignore altogether.
+  \emph{CDE/Motif} should be ignored.
 
   After changing the look-and-feel in \emph{Global Options~/
   Appearance}, it is advisable to restart Isabelle/jEdit in order to