Commit 7a140e62 authored by Ralf Jung's avatar Ralf Jung
Browse files

add ad-hoc-timing-id to early debug info

parent 8d9e688c
......@@ -34,6 +34,9 @@ set -eo pipefail
status "[buildjob] Using CI branch $(cd ci && git rev-parse --abbrev-ref HEAD) ($(cd ci && git rev-parse HEAD))"
status "[buildjob] Pipeline source: $CI_PIPELINE_SOURCE; commit branch (empty for MRs): $CI_COMMIT_BRANCH"
if [[ "$CI_RUNNER_DESCRIPTION" == "coop-timing" && -n "$TIMING_AD_HOC_ID" ]]; then
status "[buildjob] Ad-hoc timing run with ID $TIMING_AD_HOC_ID"
fi
OCAML=${OCAML:-ocaml-base-compiler.4.08.1}
MAKE_TARGET=${MAKE_TARGET:-all}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment