commit 8dce194d9a5ddc8a7c5f2c076be1afb2bc74fbe3
author Davide Pesavento <davidepesa@gmail.com> Sat Oct 02 22:31:26 2021 -0400
committer Davide Pesavento <davidepesa@gmail.com> Sat Oct 02 22:31:26 2021 -0400
tree 794f5aa5f8fef725c6a74125dba6e7a5fa3fbf12
parent 9f14dcd319dba95545f2c850ef4b3f5a6b6882bc

ci: replace Travis with GitHub Actions

Change-Id: Id9f6bc462115c1c49f02b8b75d65304f777e0ffd

.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