| author | wenzelm |
| Thu, 13 Oct 2016 11:43:40 +0200 | |
| changeset 64185 | f4d5eb78b8a5 |
| parent 64021 | 1e23caac8757 |
| child 64200 | 2e6597279d38 |
| permissions | -rwxr-xr-x |
|
64021
1e23caac8757
basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff
changeset
|
1 |
#!/usr/bin/env bash |
|
1e23caac8757
basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff
changeset
|
2 |
# |
|
1e23caac8757
basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff
changeset
|
3 |
# DESCRIPTION: build history versions from another repository clone |
|
1e23caac8757
basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff
changeset
|
4 |
|
|
1e23caac8757
basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff
changeset
|
5 |
|
|
1e23caac8757
basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff
changeset
|
6 |
THIS="$(cd "$(dirname "$0")"; pwd)" |
|
1e23caac8757
basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff
changeset
|
7 |
|
|
1e23caac8757
basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff
changeset
|
8 |
"$THIS/build" jars || exit $? |
|
1e23caac8757
basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff
changeset
|
9 |
|
|
1e23caac8757
basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff
changeset
|
10 |
exec "$THIS/../bin/isabelle_java" isabelle.Build_History "$@" |