author | wenzelm |
Fri, 11 Nov 2022 23:04:55 +0100 | |
changeset 76508 | ecb9e6d29698 |
parent 75518 | cb4af8c6152f |
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 |
# |
75518
cb4af8c6152f
clarified remote vs. local build_history: operate on hg_sync directory instead of repository;
wenzelm
parents:
74038
diff
changeset
|
3 |
# DESCRIPTION: build other Isabelle from sync_repos directory |
64021
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 |
|
74038
b4f57bfe82e7
more robust "isabelle build_scala" as separate tool;
wenzelm
parents:
74017
diff
changeset
|
8 |
"$THIS/../bin/isabelle" scala_build -q || exit $? |
b4f57bfe82e7
more robust "isabelle build_scala" as separate tool;
wenzelm
parents:
74017
diff
changeset
|
9 |
"$THIS/../bin/isabelle_java" isabelle.Build_History "$@" |