# HG changeset patch
# User wenzelm
# Date 1620734619 -7200
# Node ID 02351b514b34f2b74b92aed5ae3da9d4e760d63e
# Parent  5e12dad8d09b4037a73a21a9ce3bb3f3066db8f3
proper jEdit.props (amending ff716ecb0805);

diff -r 5e12dad8d09b -r 02351b514b34 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