# HG changeset patch
# User wenzelm
# Date 1472499984 -7200
# Node ID dd327befd2ef2ed9965d2d92d9aa7bfc34be1328
# Parent  4c00ba1ad11a1044e6eb91553befe9a138b7cf8d
clarified default;

diff -r 4c00ba1ad11a -r dd327befd2ef 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