Admin/init_components
changeset 48166 1bee47c0c278
parent 48154 2709937c7430
child 48448 94c11abc5a52
equal deleted inserted replaced
48165:d07a0b9601aa 48166:1bee47c0c278
    14   else
    14   else
    15     echo "Warning: no component found in ${LOCATION}" >&2
    15     echo "Warning: no component found in ${LOCATION}" >&2
    16   fi
    16   fi
    17 }
    17 }
    18 
    18 
    19 for COMPONENTS_FILE in "${ISABELLE_HOME}/Admin/components" "${ISABELLE_HOME}/Admin/components.${ML_PLATFORM}"
    19 while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
    20 do
    20 do
    21   while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
    21   case "${REPLY}" in
    22   do
    22     \#* | "") ;;
    23     case "${REPLY}" in
    23     /*) init_component_liberal "${REPLY}" ;;
    24       \#* | "") ;;
    24     *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
    25       /*) init_component_liberal "${REPLY}" ;;
    25   esac
    26       *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
    26 done < "${ISABELLE_HOME}/Admin/components"
    27     esac
       
    28   done < "${COMPONENTS_FILE}"
       
    29 done