diff --git a/etc/ci/describe-system-config.sh b/etc/ci/describe-system-config.sh index dbcba70e782..e317c11d810 100755 --- a/etc/ci/describe-system-config.sh +++ b/etc/ci/describe-system-config.sh @@ -1,20 +1,20 @@ -#!/usr/bin/env bash +#!/bin/sh -cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" +cd -- "$( dirname -- "$0" )" cd ../.. -function run() { +run() { "${SHELL}" -c "$@" || true } if [ ! -z "$CI" ]; then - function group() { + group() { echo "::group::$@" run "$@" echo "::endgroup::" } else - function group() { run "$@"; } + group() { run "$@"; } fi group lscpu @@ -22,6 +22,11 @@ group uname -a group lsb_release -a group ulimit -aH group ulimit -aS +group "cat /etc/os-release" +group "cat /proc/cpuinfo" +group "cat /proc/meminfo" +group "apk info" +group "dpkg -l" group ghc --version group gcc --version group ocamlc -config @@ -30,3 +35,4 @@ group coqc --version group "true | coqtop" group etc/machine.sh group "echo PATH=$PATH" +group "echo SHELL=$SHELL"