# HG changeset patch
# User wenzelm
# Date 1343052806 -7200
# Node ID 94c11abc5a52174a94c4d98a25651d36a0c08ad4
# Parent  ef600ce4559c67320b27ea6de4745e7f38d03004
clarified init_component: always liberal;
reduced divergence of clone from lib/scripts/getsettings;

diff -r ef600ce4559c -r 94c11abc5a52 Admin/init_components
--- a/Admin/init_components	Mon Jul 23 15:59:14 2012 +0200
+++ b/Admin/init_components	Mon Jul 23 16:13:26 2012 +0200
@@ -5,22 +5,11 @@
 # init_components - bash source script to initialize components
 # as specified in the Admin directory
 
-function init_component_liberal
-{
-  local LOCATION="$1"
-  if [[ -d "${LOCATION}" ]]
-  then
-    init_component "${LOCATION}"
-  else
-    echo "Warning: no component found in ${LOCATION}" >&2
-  fi
-}
-
-while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
+while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
 do
-  case "${REPLY}" in
+  case "$REPLY" in
     \#* | "") ;;
-    /*) init_component_liberal "${REPLY}" ;;
-    *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
+    /*) init_component "$REPLY" ;;
+    *) init_component "$COMPONENT/$REPLY" ;;
   esac
-done < "${ISABELLE_HOME}/Admin/components"
+done < "$ISABELLE_HOME/Admin/components"
diff -r ef600ce4559c -r 94c11abc5a52 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Mon Jul 23 15:59:14 2012 +0200
+++ b/lib/scripts/getsettings	Mon Jul 23 16:13:26 2012 +0200
@@ -163,8 +163,7 @@
   esac
 
   if [ ! -d "$COMPONENT" ]; then
-    echo >&2 "Missing Isabelle component directory: \"$COMPONENT\""
-    exit 2
+    echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
   elif [ -z "$ISABELLE_COMPONENTS" ]; then
     ISABELLE_COMPONENTS="$COMPONENT"
   else