diff --git a/buildjob b/buildjob index 1bae0dc8eb481976decb72d3d1ebe2eb8c22090d..bcec710c7045b46dbb1345179bcec0cbd022069f 100755 --- a/buildjob +++ b/buildjob @@ -26,7 +26,7 @@ echo_color "$BOLDGREEN" "[buildjob] Perfoming build" time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi echo_color "$BOLDGREEN" "[buildjob] Build time summary" -cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt +cat build-log.txt | egrep "(real|user): [0-9]" | tee build-time.txt # maybe validate if [[ -n "$VALIDATE" ]]; then