diff --git a/buildjob b/buildjob index a536d0a3b135b53795047ad2a8aefae818d25a68..13c3c16857c94b92d8bd090bab7f64d478a4148a 100755 --- a/buildjob +++ b/buildjob @@ -32,12 +32,6 @@ if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi echo_color "$BOLDGREEN" "[buildjob] Build time summary" cat build-log.txt | egrep "(real|user): [0-9]" | tee build-time.txt -# maybe validate -if [[ -n "$VALIDATE" ]]; then - echo_color "$BOLDGREEN" "[buildjob] Performing validation" - make validate -fi - # maybe submit timing information if [[ -n "$TIMING_PROJECT" && -n "$TIMING_CONF" ]]; then echo_color "$BOLDGREEN" "[buildjob] Submitting timing information to coq-speed" @@ -57,26 +51,6 @@ if [[ -n "$TIMING_PROJECT" && -n "$TIMING_CONF" ]]; then --data-binary @- < build-time.txt fi -# maybe generate and upload documentation -if [[ -n "$DOC_DIR" && "$CI_COMMIT_REF_NAME" == "${DOC_BRANCH:-master}" ]]; then - echo_color "$BOLDGREEN" "Publishing documentation from branch $CI_COMMIT_REF_NAME to $DOC_DIR" - # check if we have the secret - if [[ -z "$DOC_KEY" ]]; then - echo_color "$BOLDRED" "[buildjob] DOC_KEY variable is missing" - exit 1 - fi - - # We need a custom wrapper around SSH to use our settings, and ssh-agent for the key - eval $(ssh-agent -s) - echo "${DOC_KEY}" | tr -d '\r' | ssh-add - - export GIT_SSH=$(readlink -e ci/ssh) - - # Generate documentation - make html - # Upload documentation - rsync -a --delete -e "$GIT_SSH" html/ "$DOC_DIR/" -fi - # maybe create opam package if [[ -n "$OPAM_PKG" && "$CI_COMMIT_REF_NAME" == "${OPAM_PKG_BRANCH:-master}" ]]; then echo_color "$BOLDGREEN" "[buildjob] Releasing package on opam" @@ -102,3 +76,29 @@ if [[ -n "$OPAM_PKG" && "$CI_COMMIT_REF_NAME" == "${OPAM_PKG_BRANCH:-master}" ]] -F "variables[OPAM_PREFIX]=$OPAM_PKG_PREFIX" echo # there's no newline here otherwise fi + +# maybe validate +if [[ -n "$VALIDATE" ]]; then + echo_color "$BOLDGREEN" "[buildjob] Performing validation" + make validate +fi + +# maybe generate and upload documentation +if [[ -n "$DOC_DIR" && "$CI_COMMIT_REF_NAME" == "${DOC_BRANCH:-master}" ]]; then + echo_color "$BOLDGREEN" "Publishing documentation from branch $CI_COMMIT_REF_NAME to $DOC_DIR" + # check if we have the secret + if [[ -z "$DOC_KEY" ]]; then + echo_color "$BOLDRED" "[buildjob] DOC_KEY variable is missing" + exit 1 + fi + + # We need a custom wrapper around SSH to use our settings, and ssh-agent for the key + eval $(ssh-agent -s) + echo "${DOC_KEY}" | tr -d '\r' | ssh-add - + export GIT_SSH=$(readlink -e ci/ssh) + + # Generate documentation + make html + # Upload documentation + rsync -a --delete -e "$GIT_SSH" html/ "$DOC_DIR/" +fi