equal
deleted
inserted
replaced
157 fi |
157 fi |
158 done |
158 done |
159 export ISABELLE_SCALA_SERVICES |
159 export ISABELLE_SCALA_SERVICES |
160 } |
160 } |
161 export -f isabelle_scala_service |
161 export -f isabelle_scala_service |
|
162 |
|
163 #Special directories |
|
164 function isabelle_directory () |
|
165 { |
|
166 local X="" |
|
167 for X in "$@" |
|
168 do |
|
169 if [ -z "$ISABELLE_DIRECTORIES" ]; then |
|
170 ISABELLE_DIRECTORIES="$X" |
|
171 else |
|
172 ISABELLE_DIRECTORIES="$ISABELLE_DIRECTORIES:$X" |
|
173 fi |
|
174 done |
|
175 export ISABELLE_DIRECTORIES |
|
176 } |
|
177 export -f isabelle_directory |
162 |
178 |
163 #administrative build |
179 #administrative build |
164 if [ -e "$ISABELLE_HOME/Admin/build" ]; then |
180 if [ -e "$ISABELLE_HOME/Admin/build" ]; then |
165 function isabelle_admin_build () |
181 function isabelle_admin_build () |
166 { |
182 { |