diff -r cc1557643ab1 -r 8addfff5965a src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Wed Jan 20 14:43:21 2016 +0100 +++ b/src/Doc/JEdit/JEdit.thy Wed Jan 20 15:17:03 2016 +0100 @@ -336,8 +336,7 @@ in mind that this extra variance of GUI functionality is unlikely to work in arbitrary combinations. The platform-independent \<^emph>\Metal\ and \<^emph>\Nimbus\ should always work on all platforms, although they are technically and - stylistically outdated. The historic \<^emph>\CDE/Motif\ on Linux should be - ignored. + stylistically outdated. The historic \<^emph>\CDE/Motif\ should be ignored. After changing the look-and-feel in \<^emph>\Global Options~/ Appearance\, Isabelle/jEdit should be restarted to take full effect.