| author | haftmann |
| Tue, 26 Jun 2012 22:23:28 +0200 | |
| changeset 48151 | a80595d4f850 |
| parent 48150 | c97656ff4154 |
| child 48152 | f06697f776b0 |
| permissions | -rw-r--r-- |
|
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 |
|
|
c97656ff4154
snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff
changeset
|
8 |
function init_component_liberal |
|
c97656ff4154
snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff
changeset
|
9 |
{
|
|
c97656ff4154
snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff
changeset
|
10 |
local LOCATION="$1" |
|
48151
a80595d4f850
correction: proper initialization of existing component
haftmann
parents:
48150
diff
changeset
|
11 |
if [[ -d "${LOCATION}" ]]
|
|
a80595d4f850
correction: proper initialization of existing component
haftmann
parents:
48150
diff
changeset
|
12 |
then |
|
a80595d4f850
correction: proper initialization of existing component
haftmann
parents:
48150
diff
changeset
|
13 |
init_component "${LOCATION}"
|
|
a80595d4f850
correction: proper initialization of existing component
haftmann
parents:
48150
diff
changeset
|
14 |
else |
|
a80595d4f850
correction: proper initialization of existing component
haftmann
parents:
48150
diff
changeset
|
15 |
echo "Warning: no component found in ${LOCATION}"
|
|
a80595d4f850
correction: proper initialization of existing component
haftmann
parents:
48150
diff
changeset
|
16 |
fi |
|
48150
c97656ff4154
snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff
changeset
|
17 |
} |
|
c97656ff4154
snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff
changeset
|
18 |
|
|
c97656ff4154
snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff
changeset
|
19 |
while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
|
|
c97656ff4154
snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff
changeset
|
20 |
do |
|
c97656ff4154
snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff
changeset
|
21 |
case "${REPLY}" in
|
|
c97656ff4154
snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff
changeset
|
22 |
\#* | "") ;; |
|
c97656ff4154
snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff
changeset
|
23 |
/*) init_component_liberal "${REPLY}" ;;
|
|
c97656ff4154
snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff
changeset
|
24 |
*) init_component_liberal "${COMPONENT}/${REPLY}" ;;
|
|
c97656ff4154
snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff
changeset
|
25 |
esac |
|
c97656ff4154
snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff
changeset
|
26 |
done < "${ISABELLE_HOME}/Admin/components"
|