# HG changeset patch
# User wenzelm
# Date 1557412117 -7200
# Node ID 6778fdbd6c5df7be28afd279ac1690ae311d7bfc
# Parent  62a6c1257c053883648f612154dd31d20d3a3703
tuned;

diff -r 62a6c1257c05 -r 6778fdbd6c5d src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Thu May 09 15:56:14 2019 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Thu May 09 16:28:37 2019 +0200
@@ -2157,7 +2157,8 @@
   \<^path>\<open>$ISABELLE_HOME_USER/etc/settings\<close>. Also add
   \<^verbatim>\<open>isabelle_fonts_hinted=false\<close> to
   \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close> to avoid problems of the old
-  font renderer with hinting.
+  font renderer with hinting. Run the application from the command-line as
+  @{tool jedit}.
 
   \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and \<^verbatim>\<open>C+MINUS\<close> for adjusting the
   editor font size depend on platform details and national keyboards.