equal
deleted
inserted
replaced
|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # Do not run this script manually, it is only to be executed by Jenkins. |
|
4 |
|
5 set -x |
|
6 set -e |
|
7 |
|
8 PROFILE="$1" |
|
9 shift |
|
10 |
|
11 bin/isabelle components -a |
|
12 bin/isabelle jedit -bf |
|
13 bin/isabelle "ci_build_$PROFILE" "$@" |