diff -r 9cb0abdf7c07 -r c97656ff4154 Admin/init_components
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/init_components	Tue Jun 26 22:09:34 2012 +0200
@@ -0,0 +1,22 @@
+# -*- shell-script -*- :mode=shellscript:
+#
+# Author: Florian Haftmann, TU Muenchen
+#
+# init_components - bash source script to initialize components
+# as specified in the Admin directory
+
+function init_component_liberal
+{
+  local LOCATION="$1"
+  [[ -d "${LOCATION}" ]] || echo "Warning: no component found in ${LOCATION}" && return
+  init_component "${LOCATION}"
+}
+
+while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
+do
+  case "${REPLY}" in
+    \#* | "") ;;
+    /*) init_component_liberal "${REPLY}" ;;
+    *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
+  esac
+done < "${ISABELLE_HOME}/Admin/components"