Admin/jenkins/run_build
changeset 63288 e0513d6e4916
child 69137 90fce429e1bc
equal deleted inserted replaced
63283:a59801b7f125 63288:e0513d6e4916
       
     1 #!/usr/bin/env bash
       
     2 #
       
     3 # Do not run this script manually, it is only to be executed by Jenkins.
       
     4 
       
     5 set -x
       
     6 set -e
       
     7 
       
     8 PROFILE="$1"
       
     9 shift
       
    10 
       
    11 bin/isabelle components -a
       
    12 bin/isabelle jedit -bf
       
    13 bin/isabelle "ci_build_$PROFILE" "$@"