Admin/init_components
author wenzelm
Wed, 15 Aug 2012 12:36:38 +0200
changeset 48814 d488a5f25bf6
parent 48448 94c11abc5a52
child 48842 ac976e51cb67
permissions -rw-r--r--
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");

# -*- 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"