Admin/jenkins/run_build
author wenzelm
Tue, 16 Jan 2018 09:58:17 +0100
changeset 67445 4311845b0412
parent 63288 e0513d6e4916
child 69137 90fce429e1bc
permissions -rwxr-xr-x
tuned document;
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" "$@"