author | blanchet |
Fri, 16 Dec 2016 22:54:14 +0100 | |
changeset 64576 | ce8802dc3145 |
parent 63288 | e0513d6e4916 |
child 69137 | 90fce429e1bc |
permissions | -rwxr-xr-x |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
1 |
#!/usr/bin/env bash |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
2 |
# |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
3 |
# Do not run this script manually, it is only to be executed by Jenkins. |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
4 |
|
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
5 |
set -x |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
6 |
set -e |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
7 |
|
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
8 |
PROFILE="$1" |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
9 |
shift |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
10 |
|
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
11 |
bin/isabelle components -a |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
12 |
bin/isabelle jedit -bf |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
13 |
bin/isabelle "ci_build_$PROFILE" "$@" |