mathlib3

b4dc9128 - ci(*): run style lint in parallel job, fix update-copy-mod-doc-exceptions.sh (#4513)

ci(*): run style lint in parallel job, fix update-copy-mod-doc-exceptions.sh (#4513) Followup to #4486: - run the linter in a separate parallel job, per request - the update-*.sh script now correctly generates a full exceptions file - add some more comments to the shell scripts