author | wenzelm |
Fri, 17 Aug 2012 11:23:57 +0200 | |
changeset 48835 | 574042d14fd9 |
parent 48448 | 94c11abc5a52 |
child 48842 | ac976e51cb67 |
permissions | -rw-r--r-- |
# -*- 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"