FYI CI now merges master

Stream: lean4 dev

[Gabriel Ebner]

I didn't realize that until now but apparently the upgrade to actions/checkout@v3 changed its default behavior.

[Gabriel Ebner]

It now merges master into the PR commit.

[Sebastian Ullrich]

I'm quite sure it already did that before

[Gabriel Ebner]

It certainly doesn't happen in mathlib though. Maybe it's because we're using the auto merge feature in lean4?

[Sebastian Ullrich]

Mmh interesting, the instructions on how to do that explicitly seem to be unchanged from v2 to v3 https://github.com/actions/checkout/tree/v2.6.0#Checkout-pull-request-HEAD-commit-instead-of-merge-commit