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