etc/settings
changeset 61500 56a167b31a7f
parent 61355 31829cf53f5d
child 61735 a1b779ee035c
equal deleted inserted replaced
61499:4efe9a6dd212 61500:56a167b31a7f
   122 
   122 
   123 ###
   123 ###
   124 ### Rendering information
   124 ### Rendering information
   125 ###
   125 ###
   126 
   126 
   127 ISABELLE_FONTS="$ISABELLE_HOME/lib/fonts/IsabelleText.ttf:$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"
       
   128 ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
   127 ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
   129 
   128 
   130 
   129 
   131 ###
   130 ###
   132 ### Misc old-style settings
   131 ### Misc old-style settings