etc/settings
changeset 43484 51b8043a8cf5
parent 41968 7f5c9bd991be
child 43515 55160cf1e4f6
--- a/etc/settings	Mon Jun 20 22:48:41 2011 +0200
+++ b/etc/settings	Mon Jun 20 23:19:38 2011 +0200
@@ -188,7 +188,7 @@
 ### Rendering information
 ###
 
-ISABELLE_FONT_FAMILY="IsabelleText"
+ISABELLE_FONTS="$ISABELLE_HOME/lib/fonts/IsabelleText.ttf:$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"
 ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"