obsolete -- was mostly about 'export_code';
authorwenzelm
Sat Apr 06 22:09:41 2019 +0200 (6 months ago)
changeset 700736b0e4ba2062c
parent 70072 54dc58086351
child 70074 b718a64d0d09
obsolete -- was mostly about 'export_code';
src/Doc/JEdit/JEdit.thy
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Sat Apr 06 22:05:25 2019 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Sat Apr 06 22:09:41 2019 +0200
     1.3 @@ -2108,12 +2108,6 @@
     1.4  chapter \<open>Known problems and workarounds \label{sec:problems}\<close>
     1.5  
     1.6  text \<open>
     1.7 -  \<^item> \<^bold>\<open>Problem:\<close> Odd behavior of some diagnostic commands with global
     1.8 -  side-effects, like writing a physical file.
     1.9 -
    1.10 -  \<^bold>\<open>Workaround:\<close> Copy/paste complete command text from elsewhere, or disable
    1.11 -  continuous checking temporarily.
    1.12 -
    1.13    \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and \<^verbatim>\<open>C+MINUS\<close> for adjusting the
    1.14    editor font size depend on platform details and national keyboards.
    1.15