From 8324acefba3ffef86b4c5eca3c961ce69dc4dd02 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Thu, 21 Jun 2018 21:12:52 +0200
Subject: [PATCH] add pretty header for build time information
---
buildjob | 9 +++++----
1 file changed, 5 insertions(+), 4 deletions(-)
diff --git a/buildjob b/buildjob
index ad4036f..e11aa3b 100755
--- a/buildjob
+++ b/buildjob
@@ -47,15 +47,16 @@ fi
# maybe submit timing information
if [[ -n "$TIMING_PROJECT" && -n "$TIMING_CONF" ]]; then
- echo_color "$BOLDGREEN" "[buildjob] Submitting timing information to coq-speed"
+ # collect all information into one file
+ echo_color "$BOLDGREEN" "[buildjob] Build performance information"
+ find -name "*.v.perf" -print0 | xargs -0 cat > build-times.txt
+ cat build-times.txt
# check if we have the secret
+ echo_color "$BOLDGREEN" "[buildjob] Submitting timing information to coq-speed"
if [[ -z "$TIMING_SECRET" ]]; then
echo_color "$BOLDRED" "[buildjob] TIMING_SECRET variable is missing"
exit 1
fi
- # collect all information into one file
- find -name "*.v.perf" -print0 | xargs -0 cat > build-times.txt
- cat build-times.txt
# Submit to webhook endpoint
curl --fail -sS -X POST https://coq-speed.mpi-sws.org/webhook/build_times \
--user "$TIMING_SECRET" \
--
GitLab