author | wenzelm |
Sat, 09 Nov 2013 18:00:36 +0100 | |
changeset 54381 | 9c1f21365326 |
parent 54380 | 209596f56c05 |
child 54382 | 75623b4d6251 |
--- a/src/Doc/JEdit/JEdit.thy Sat Nov 09 12:47:32 2013 +0100 +++ b/src/Doc/JEdit/JEdit.thy Sat Nov 09 18:00:36 2013 +0100 @@ -229,7 +229,8 @@ finished, and is today (2013) lagging a bit behind further development of Swing and GTK.} - \item[Windows] Regular \emph{Windows} is used by default. + \item[Windows] Regular \emph{Windows} is used by default, but + \emph{Windows Classic} also works. \item[Mac OS X] Regular \emph{Mac OS X} is used by default.