| author | wenzelm |
| Fri, 16 Jul 2021 13:18:54 +0200 | |
| changeset 74017 | b4e6b82fdb9e |
| parent 73705 | ac07f6be27ea |
| child 74038 | b4f57bfe82e7 |
| 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 |
|
|
73705
ac07f6be27ea
avoid unexpected output+behaviour when CDPATH is set
kleing
parents:
64223
diff
changeset
|
5 |
unset CDPATH |
|
64021
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 |
|
|
74017
b4e6b82fdb9e
more direct isabelle_scala_build: always enabled, no "Admin" requirement;
wenzelm
parents:
73705
diff
changeset
|
8 |
env ISABELLE_SETUP_CLASSPATH_SKIP=true "$THIS/../bin/isabelle" java isabelle.setup.Setup build > /dev/null || exit $? |
|
64021
1e23caac8757
basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff
changeset
|
9 |
exec "$THIS/../bin/isabelle_java" isabelle.Build_History "$@" |