src/Tools/jEdit/src/jEdit.props
changeset 63726 dd327befd2ef
parent 63455 019856db2bb6
child 63737 fb0ae6b60491
     1.1 --- a/src/Tools/jEdit/src/jEdit.props	Fri Aug 26 11:58:19 2016 +0200
     1.2 +++ b/src/Tools/jEdit/src/jEdit.props	Mon Aug 29 21:46:24 2016 +0200
     1.3 @@ -255,6 +255,7 @@
     1.4  plugin.MacOSXPlugin.disableOption=true
     1.5  prev-bracket.shortcut2=C+e C+8
     1.6  print.font=IsabelleText
     1.7 +print.glyphVector=true
     1.8  recent-buffer.shortcut2=C+CIRCUMFLEX
     1.9  restore.remote=false
    1.10  restore=false