From 45c7be45f5859972b869ffd8193426332e579735 Mon Sep 17 00:00:00 2001 From: damiano Date: Tue, 21 Jan 2025 11:30:30 +0000 Subject: [PATCH] fix(CI): use `gawk` instead of `awk` (#20909) This probably makes running the import diff script locally friendlier for MacOS users that have `gawk` installed. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/import.20diff.20bot) --- scripts/import_trans_difference.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/import_trans_difference.sh b/scripts/import_trans_difference.sh index 30902e69f971e..8c72ba69ef2ed 100755 --- a/scripts/import_trans_difference.sh +++ b/scripts/import_trans_difference.sh @@ -67,7 +67,7 @@ git checkout "${currCommit}" printf '\n\n
Import changes for all files\n\n%s\n\n
\n' "$( printf "|Files|Import difference|\n|-|-|\n" - (awk -F, -v all="${all}" -v ghLimit='261752' -v newFiles="$( + (gawk -F, -v all="${all}" -v ghLimit='261752' -v newFiles="$( # we pass the "A"dded files with respect to master, converting them to module names git diff --name-only --diff-filter=A master | tr '\n' , | sed 's=\.lean,=,=g; s=/=.=g' )" '