Admin/init_components
changeset 48154 2709937c7430
parent 48152 f06697f776b0
child 48166 1bee47c0c278
equal deleted inserted replaced
48153:210043eb4c88 48154:2709937c7430
    10   local LOCATION="$1"
    10   local LOCATION="$1"
    11   if [[ -d "${LOCATION}" ]]
    11   if [[ -d "${LOCATION}" ]]
    12   then
    12   then
    13     init_component "${LOCATION}"
    13     init_component "${LOCATION}"
    14   else
    14   else
    15     echo "Warning: no component found in ${LOCATION}"
    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 for COMPONENTS_FILE in "${ISABELLE_HOME}/Admin/components" "${ISABELLE_HOME}/Admin/components.${ML_PLATFORM}"
    20 do
    20 do