Admin/jenkins/run_build
author Lars Hupel <lars.hupel@mytum.de>
Sat, 11 Jun 2016 17:23:24 +0200
changeset 63288 e0513d6e4916
child 69137 90fce429e1bc
permissions -rwxr-xr-x
start moving actual Jenkins build scripts into the repository
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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" "$@"