--- a/src/Doc/JEdit/JEdit.thy Tue May 11 13:45:09 2021 +0200
+++ b/src/Doc/JEdit/JEdit.thy Tue May 11 14:03:39 2021 +0200
@@ -206,7 +206,7 @@
is no longer affected by change of default properties.
Users may modify their keymap later, but this can lead to conflicts with
- \<^verbatim>\<open>shortcut\<close> properties in \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.
+ \<^verbatim>\<open>shortcut\<close> properties in \<^file>\<open>$JEDIT_HOME/dist/properties/jEdit.props\<close>.
The action @{action_def "isabelle.keymap-merge"} helps to resolve pending
Isabelle keymap changes wrt. the current jEdit keymap; non-conflicting