diff --git a/Jenkinsfile b/Jenkinsfile index 006a445..ad7ef8b 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -254,8 +254,7 @@ EOF esac fi fi - if ! cat </dev/null; then - echo "warning: metrics push failed for suite=${suite}" >&2 + cat > build/pushgateway-metrics.prom </dev/null; then + echo "warning: metrics push failed for suite=${suite}" >&2 fi ''' }