From 0596415f3190cf36cdc337b40acd9867bfcfa5e2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 31 Oct 2023 19:48:27 -0700 Subject: [PATCH] gcc --version, not gcc -v --- etc/ci/describe-system-config.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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