Commit 2026-10-17 13:58 4c71e7e7

ci: add --add-public-downstream to shake options (#44962) https://github.com/leanprover/lean4/pull/15630 added the lake shake --add-public-downstream and --add-downstream options, which allow specifying a single module that should be imported in every other module that would not create an import cycle. This should probably replace the text-based linter.checkInitImports, but I think it is better to leave this to a separate PR. For now I just add this option to the workflow that opens shake PRs.