tuned;
authorwenzelm
Thu May 09 16:28:37 2019 +0200 (6 months ago)
changeset 702576778fdbd6c5d
parent 70256 62a6c1257c05
child 70258 b4534d72dd22
tuned;
src/Doc/JEdit/JEdit.thy
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Thu May 09 15:56:14 2019 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Thu May 09 16:28:37 2019 +0200
     1.3 @@ -2157,7 +2157,8 @@
     1.4    \<^path>\<open>$ISABELLE_HOME_USER/etc/settings\<close>. Also add
     1.5    \<^verbatim>\<open>isabelle_fonts_hinted=false\<close> to
     1.6    \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close> to avoid problems of the old
     1.7 -  font renderer with hinting.
     1.8 +  font renderer with hinting. Run the application from the command-line as
     1.9 +  @{tool jedit}.
    1.10  
    1.11    \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and \<^verbatim>\<open>C+MINUS\<close> for adjusting the
    1.12    editor font size depend on platform details and national keyboards.