Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • iris/ci
  • msammler/ci
  • snyke7/ci
3 results
Show changes
Commits on Source (1)
......@@ -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