isabelle: Admin/init_components@d488a5f25bf6 (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
48448 94c11abc5a52 clarified init_component: always liberal; wenzelm parents: 48166 diff changeset	8	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	9	do
48448 94c11abc5a52 clarified init_component: always liberal; wenzelm parents: 48166 diff changeset	10	case "$REPLY" in
48166 1bee47c0c278 no ml-platform-specific components haftmann parents: 48154 diff changeset	11	\#* \| "") ;;
48448 94c11abc5a52 clarified init_component: always liberal; wenzelm parents: 48166 diff changeset	12	/*) init_component "$REPLY" ;;
94c11abc5a52 clarified init_component: always liberal; wenzelm parents: 48166 diff changeset	13	*) init_component "$COMPONENT/$REPLY" ;;
48166 1bee47c0c278 no ml-platform-specific components haftmann parents: 48154 diff changeset	14	esac
48448 94c11abc5a52 clarified init_component: always liberal; wenzelm parents: 48166 diff changeset	15	done < "$ISABELLE_HOME/Admin/components"

author	wenzelm
	Wed, 15 Aug 2012 12:36:38 +0200
changeset 48814	d488a5f25bf6
parent 48448	94c11abc5a52
child 48842	ac976e51cb67
permissions	-rw-r--r--