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;
# -*- shell-script -*- :mode=shellscript:
#
# Author: Florian Haftmann, TU Muenchen
#
# init_components - bash source script to initialize components
# as specified in the Admin directory
while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
do
case "$REPLY" in
\#* | "") ;;
/*) init_component "$REPLY" ;;
*) init_component "$COMPONENT/$REPLY" ;;
esac
done < "$ISABELLE_HOME/Admin/components"