Admin/init_components
author wenzelm
Fri, 17 Aug 2012 11:37:14 +0200
changeset 48836 90a0af19004c
parent 48448 94c11abc5a52
child 48842 ac976e51cb67
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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"