Skip to content

Commit

Permalink
fix(CI): use gawk instead of awk (#20909)
Browse files Browse the repository at this point in the history
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)
  • Loading branch information
adomani committed Jan 21, 2025
1 parent 1264ce9 commit 45c7be4
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion scripts/import_trans_difference.sh
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ git checkout "${currCommit}"

printf '\n\n<details><summary>Import changes for all files</summary>\n\n%s\n\n</details>\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'
)" '
Expand Down

0 comments on commit 45c7be4

Please sign in to comment.