diff --git a/etc/ci/describe-system-config.sh b/etc/ci/describe-system-config.sh index dbcba70e78..a2c47cdbb9 100755 --- a/etc/ci/describe-system-config.sh +++ b/etc/ci/describe-system-config.sh @@ -1,20 +1,26 @@ -#!/usr/bin/env bash +#!/bin/sh -cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" +cd -- "$( dirname -- "$0" )" cd ../.. -function run() { - "${SHELL}" -c "$@" || true -} +if [ ! -z "${SHELL}" ]; then + run() { + "${SHELL}" -c "$@" || true + } +else + run() { + /bin/sh -c "$@" || true + } +fi if [ ! -z "$CI" ]; then - function group() { + group() { echo "::group::$@" run "$@" echo "::endgroup::" } else - function group() { run "$@"; } + group() { run "$@"; } fi group lscpu @@ -22,11 +28,19 @@ 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 ghc -v group gcc --version +group gcc -v group ocamlc -config group coqc --config group coqc --version group "true | coqtop" group etc/machine.sh group "echo PATH=$PATH" +group "echo SHELL=$SHELL"