no longer force STIX fonts onto the user -- NB: STIXv1.0.0 is outdated and Mac OS 10.7 ships its own copy of STIX already;
authorwenzelm
Wed, 01 Aug 2012 12:14:56 +0200
changeset 4964681c81f13d152
parent 49645 2f230b617541
child 49647 c028cf680a3e
no longer force STIX fonts onto the user -- NB: STIXv1.0.0 is outdated and Mac OS 10.7 ships its own copy of STIX already;
Admin/MacOS/App1/script
     1.1 --- a/Admin/MacOS/App1/script	Wed Aug 01 11:55:18 2012 +0200
     1.2 +++ b/Admin/MacOS/App1/script	Wed Aug 01 12:14:56 2012 +0200
     1.3 @@ -59,18 +59,6 @@
     1.4  fi
     1.5  
     1.6  
     1.7 -# enforce fonts
     1.8 -
     1.9 -if [ ! -f "$HOME/Library/Fonts/STIXGeneral.ttf" -a ! -f "$HOME/Library/Fonts/STIXGeneral.otf" ]
    1.10 -then
    1.11 -  cp -f "$THIS/STIXv1.0.0/Fonts"/STIXGeneral* "$HOME/Library/Fonts/"
    1.12 -  sleep 3
    1.13 -fi
    1.14 -
    1.15 -EMACS_OPTIONS["${#EMACS_OPTIONS[@]}"]="-x"
    1.16 -EMACS_OPTIONS["${#EMACS_OPTIONS[@]}"]="true"
    1.17 -
    1.18 -
    1.19  # run interface with error feedback
    1.20  
    1.21  ISABELLE_INTERFACE_CHOICE="$("$ISABELLE_TOOL" getenv -b ISABELLE_INTERFACE_CHOICE)"