add pretty header for build time information

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" \