isabelle: Admin/init_components@752de4e10162 (annotated)

48150 c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision; haftmann parents: diff changeset	1	# -- shell-script -- :mode=shellscript:
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision; haftmann parents: diff changeset	2	#
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision; haftmann parents: diff changeset	3	# Author: Florian Haftmann, TU Muenchen
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision; haftmann parents: diff changeset	4	#
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision; haftmann parents: diff changeset	5	# init_components - bash source script to initialize components
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision; haftmann parents: diff changeset	6	# as specified in the Admin directory
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision; haftmann parents: diff changeset	7
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision; haftmann parents: diff changeset	8	function init_component_liberal
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision; haftmann parents: diff changeset	9	{
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision; haftmann parents: diff changeset	10	local LOCATION="$1"
48151 a80595d4f850 correction: proper initialization of existing component haftmann parents: 48150 diff changeset	11	if [[ -d "${LOCATION}" ]]
a80595d4f850 correction: proper initialization of existing component haftmann parents: 48150 diff changeset	12	then
a80595d4f850 correction: proper initialization of existing component haftmann parents: 48150 diff changeset	13	init_component "${LOCATION}"
a80595d4f850 correction: proper initialization of existing component haftmann parents: 48150 diff changeset	14	else
48154 2709937c7430 prefer stderr for warnings haftmann parents: 48152 diff changeset	15	echo "Warning: no component found in ${LOCATION}" >&2
48151 a80595d4f850 correction: proper initialization of existing component haftmann parents: 48150 diff changeset	16	fi
48150 c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision; haftmann parents: diff changeset	17	}
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision; haftmann parents: diff changeset	18
48166 1bee47c0c278 no ml-platform-specific components haftmann parents: 48154 diff changeset	19	while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
48150 c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision; haftmann parents: diff changeset	20	do
48166 1bee47c0c278 no ml-platform-specific components haftmann parents: 48154 diff changeset	21	case "${REPLY}" in
1bee47c0c278 no ml-platform-specific components haftmann parents: 48154 diff changeset	22	\#* \| "") ;;
1bee47c0c278 no ml-platform-specific components haftmann parents: 48154 diff changeset	23	/*) init_component_liberal "${REPLY}" ;;
1bee47c0c278 no ml-platform-specific components haftmann parents: 48154 diff changeset	24	*) init_component_liberal "${COMPONENT}/${REPLY}" ;;
1bee47c0c278 no ml-platform-specific components haftmann parents: 48154 diff changeset	25	esac
1bee47c0c278 no ml-platform-specific components haftmann parents: 48154 diff changeset	26	done < "${ISABELLE_HOME}/Admin/components"

author	wenzelm
	Wed, 18 Jul 2012 20:01:55 +0200
changeset 48341	752de4e10162
parent 48166	1bee47c0c278
child 48448	94c11abc5a52
permissions	-rw-r--r--