proper jEdit.props (amending ff716ecb0805);
authorwenzelm
Tue, 11 May 2021 14:03:39 +0200
changeset 73925 02351b514b34
parent 73924 5e12dad8d09b
child 73926 4121fc47432b
proper jEdit.props (amending ff716ecb0805);
src/Doc/JEdit/JEdit.thy
--- 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