etc/settings
changeset 69328 4646fcb59121
parent 69311 740b14b67472
child 69412 f0b85c8aec46
     1.1 --- a/etc/settings	Thu Nov 22 17:34:30 2018 +0100
     1.2 +++ b/etc/settings	Thu Nov 22 17:34:37 2018 +0100
     1.3 @@ -162,6 +162,7 @@
     1.4  ###
     1.5  
     1.6  ISABELLE_GNUPLOT="gnuplot"
     1.7 +ISABELLE_FONTFORGE="fontforge"
     1.8  
     1.9  #ISABELLE_MLTON="/usr/bin/mlton"
    1.10  #ISABELLE_SMLNJ="/usr/bin/sml"