start moving actual Jenkins build scripts into the repository
#!/usr/bin/env bash## Do not run this script manually, it is only to be executed by Jenkins.set -xset -ePROFILE="$1"shiftbin/isabelle components -abin/isabelle jedit -bfbin/isabelle "ci_build_$PROFILE" "$@"