Admin/jenkins/run_build
author haftmann
Fri, 14 Jun 2019 08:34:27 +0000
changeset 70335 9bd8c16b6627
parent 69161 44e1c9f93755
permissions -rwxr-xr-x
using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax
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
69137
90fce429e1bc Jenkins: run ocaml_setup
Lars Hupel <lars.hupel@mytum.de>
parents: 63288
diff changeset
    13
bin/isabelle ocaml_setup
69161
44e1c9f93755 Jenkins: run ghc_setup
Lars Hupel <lars.hupel@mytum.de>
parents: 69137
diff changeset
    14
bin/isabelle ghc_setup
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    15
bin/isabelle "ci_build_$PROFILE" "$@"