Admin/init_components
changeset 48842 ac976e51cb67
parent 48448 94c11abc5a52
equal deleted inserted replaced
48841:90fe0798b83a 48842:ac976e51cb67
    10   case "$REPLY" in
    10   case "$REPLY" in
    11     \#* | "") ;;
    11     \#* | "") ;;
    12     /*) init_component "$REPLY" ;;
    12     /*) init_component "$REPLY" ;;
    13     *) init_component "$COMPONENT/$REPLY" ;;
    13     *) init_component "$COMPONENT/$REPLY" ;;
    14   esac
    14   esac
    15 done < "$ISABELLE_HOME/Admin/components"
    15 done < "$ISABELLE_HOME/Admin/components_old"