# HG changeset patch
# User wenzelm
# Date 1608288274 -3600
# Node ID 50c48773b954af671f3ca5da94c1f60ff425aaeb
# Parent  b945880827ff92e892ddcd1ac55ca39022a62d3a
more documentation;

diff -r b945880827ff -r 50c48773b954 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Thu Dec 17 13:51:37 2020 +0000
+++ b/src/Doc/JEdit/JEdit.thy	Fri Dec 18 11:44:34 2020 +0100
@@ -1317,7 +1317,8 @@
   within the visible text area. The keyboard modifier \<^verbatim>\<open>CS\<close> overrides this:
   then all defining and referencing positions are shown. This modifier may be
   configured via option @{system_option jedit_focus_modifier}; the default
-  coincides with the modifier for the above keyboard actions.
+  coincides with the modifier for the above keyboard actions. The empty string
+  means to disable this additional visual feedback.
 \<close>