src/Tools/jEdit/src/jEdit.props
changeset 57627 65fc7ae1bf66
parent 56986 43be5818a45c
child 58746 68c2cbe2fd3a
--- a/src/Tools/jEdit/src/jEdit.props	Wed Jul 23 21:02:45 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Wed Jul 23 23:08:22 2014 +0200
@@ -216,6 +216,7 @@
 isabelle.include-word-permanently.label=Include word permanently
 isabelle.exclude-word.label=Exclude word
 isabelle.exclude-word-permanently.label=Exclude word permanently
+isabelle.options.label=Isabelle options
 isabelle.reset-words.label=Reset non-permanent words
 isabelle.reset-continuous-checking.label=Reset continuous checking
 isabelle.reset-font-size.label=Reset font size