src/Tools/jEdit/src/jEdit.props
changeset 56581 af3e6576e680
parent 56574 2b38472a4695
child 56586 5ef60881681d
--- a/src/Tools/jEdit/src/jEdit.props	Tue Apr 15 00:07:07 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Tue Apr 15 00:14:57 2014 +0200
@@ -215,7 +215,7 @@
 isabelle.include-word-permanently.label=Include word permanently
 isabelle.exclude-word.label=Exclude word
 isabelle.exclude-word-permanently.label=Exclude word permanently
-isabelle.reset-words.label=Reset words
+isabelle.reset-words.label=Reset non-permanent words
 isabelle.reset-continuous-checking.label=Reset continuous checking
 isabelle.reset-font-size.label=Reset font size
 isabelle.reset-node-required.label=Reset node required