src/Tools/jEdit/src/jEdit.props

--- a/src/Tools/jEdit/src/jEdit.props	Fri Aug 26 11:58:19 2016 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Mon Aug 29 21:46:24 2016 +0200
@@ -255,6 +255,7 @@
 plugin.MacOSXPlugin.disableOption=true
 prev-bracket.shortcut2=C+e C+8
 print.font=IsabelleText
+print.glyphVector=true
 recent-buffer.shortcut2=C+CIRCUMFLEX
 restore.remote=false
 restore=false