lean-action releases

Stream: general

[Chris Henson]

Is there an upcoming release planned for lean-action? I added a test-args input ~4 months ago, but it remains in the "unreleased" section of the changelog. (I know I can use the main branch or a specific commit, but this is not always desirable for maintenance purposes)

[Kim Morrison]

@Austin Letson, is this a question for you? (Perhaps to be answered with "please could someone else take care of this!")

[Austin Letson]

Yes, I can cut a release this week. @Chris Henson I will tag you.

[Chris Henson]

Thanks! I also noticed that with the module system now existing, we might want to similarly update the mk_all-check input to optionally include --module. Maybe not crucial to get into this release, as I don't think many (any?) projects downstream of Mathlib are using modules yet, but I'll make a PR when I get a chance.

[Sebastian Ullrich]

One alternative would be to update the script so it simply preserves any existing module annotation