diff --git a/etc/ci/describe-system-config.sh b/etc/ci/describe-system-config.sh index db767d4163..dbcba70e78 100755 --- a/etc/ci/describe-system-config.sh +++ b/etc/ci/describe-system-config.sh @@ -23,7 +23,7 @@ group lsb_release -a group ulimit -aH group ulimit -aS group ghc --version -group gcc -v +group gcc --version group ocamlc -config group coqc --config group coqc --version