clarified init_component: always liberal;
reduced divergence of clone from lib/scripts/getsettings;
--- 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"
--- 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