also set font for printing, which actually works out of the box;
authorwenzelm
Fri, 28 May 2010 15:57:25 +0200
changeset 37162 88255b98a22f
parent 37161 1754a1c17426
child 37163 a60f88087ee1
also set font for printing, which actually works out of the box;
src/Tools/jEdit/dist-template/properties/jedit.props
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Fri May 28 15:17:17 2010 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Fri May 28 15:57:25 2010 +0200
@@ -180,6 +180,7 @@
 isabelle-protocol.dock-position=bottom
 isabelle.activate.shortcut=CS+ENTER
 mode.isabelle.sidekick.showStatusWindow.label=true
+print.font=IsabelleText
 sidekick-tree.dock-position=right
 sidekick.buffer-save-parse=true
 sidekick.complete-delay=300