changeset 63288 | e0513d6e4916 |
child 69137 | 90fce429e1bc |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/jenkins/run_build Sat Jun 11 17:23:24 2016 +0200 @@ -0,0 +1,13 @@ +#!/usr/bin/env bash +# +# Do not run this script manually, it is only to be executed by Jenkins. + +set -x +set -e + +PROFILE="$1" +shift + +bin/isabelle components -a +bin/isabelle jedit -bf +bin/isabelle "ci_build_$PROFILE" "$@"