commit 90a632b673cde41a18c57bd4bfb120e22053f75d
author Davide Pesavento <davidepesa@gmail.com> Mon Oct 04 01:05:24 2021 -0400
committer Davide Pesavento <davidepesa@gmail.com> Mon Oct 04 01:05:24 2021 -0400
tree abc167f3882f36b2529b2ad696f633274126df71
parent 3d01fa3647db0b1c5ee509da14affc1f2577e01d

ci: replace Travis with GitHub Actions

Change-Id: Ic7ecccd9969e9307a68cc44c26aea1d64b84c729

.jenkins

diff --git a/.jenkins b/.jenkins
index bc1c847..da10d69 100755
--- a/.jenkins
+++ b/.jenkins
@@ -2,31 +2,25 @@
 set -e
 source .jenkins.d/util.sh
 
+if has Linux $NODE_LABELS; then
+    export PATH="${HOME}/.local/bin${PATH:+:}${PATH}"
+fi
 export CACHE_DIR=${CACHE_DIR:-/tmp}
 export WAF_JOBS=${WAF_JOBS:-1}
 [[ $JOB_NAME == *"code-coverage" ]] && export DISABLE_ASAN=yes
 
-nanos() {
-    # Cannot use date(1) because macOS does not support %N format specifier
-    python3 -c 'import time; print(int(time.time() * 1e9))'
-}
-
 for file in .jenkins.d/*; do
     [[ -f $file && -x $file ]] || continue
 
-    if [[ -n $TRAVIS ]]; then
+    if [[ -n $GITHUB_ACTIONS ]]; then
         label=$(basename "$file" | sed -E 's/[[:digit:]]+-(.*)\..*/\1/')
-        echo -ne "travis_fold:start:${label}\r"
-        echo -ne "travis_time:start:${label}\r"
-        start=$(nanos)
+        echo "::group::${label}"
     fi
 
     echo "\$ $file"
     "$file"
 
-    if [[ -n $TRAVIS ]]; then
-        finish=$(nanos)
-        echo -ne "travis_time:end:${label}:start=${start},finish=${finish},duration=$((finish-start)),event=${label}\r"
-        echo -ne "travis_fold:end:${label}\r"
+    if [[ -n $GITHUB_ACTIONS ]]; then
+        echo "::endgroup::"
     fi
 done