Admin/jenkins/run_build
author wenzelm
Fri, 19 Feb 2021 22:50:10 +0100
changeset 73254 13e206e93876
parent 69161 44e1c9f93755
child 76222 3c4e373922ca
permissions -rwxr-xr-x
provide naproche-4ad61140062f;
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" "$@"