| author | wenzelm |
| Wed, 09 May 2018 22:03:02 +0200 (2018-05-09) | |
| changeset 68131 | 62a3294edda3 |
| 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" "$@" |