obsolete -- was mostly about 'export_code';
authorwenzelm
Sat, 06 Apr 2019 22:09:41 +0200
changeset 70255 6b0e4ba2062c
parent 70254 54dc58086351
child 70256 b718a64d0d09
obsolete -- was mostly about 'export_code';
src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sat Apr 06 22:05:25 2019 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Sat Apr 06 22:09:41 2019 +0200
@@ -2108,12 +2108,6 @@
 chapter \<open>Known problems and workarounds \label{sec:problems}\<close>
 
 text \<open>
-  \<^item> \<^bold>\<open>Problem:\<close> Odd behavior of some diagnostic commands with global
-  side-effects, like writing a physical file.
-
-  \<^bold>\<open>Workaround:\<close> Copy/paste complete command text from elsewhere, or disable
-  continuous checking temporarily.
-
   \<^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.