messageFile.md

Stream: mathlib4

[Yaël Dillies]

message.txt

[Andrew Yang]

It will be fixed if one merges master

[Winston Yin (尹維晨)]

github-actions bot is commenting messageFile.md (#21286). I assume it's a bug?

[Yaël Dillies]

It means you should merge master

[Winston Yin (尹維晨)]

If only I looked two comments up... Thanks!

[Damiano Testa]

I really should have called the file please_merge_master.md.

[Winston Yin (尹維晨)]

Is it still possible to change the name to please_merge_master.md...?

[Damiano Testa]

If you are serious about this, here we go! #21676

[Eric Wieser]

Why do we checkout the current branch in that CI script?

[Eric Wieser]

Can't we use git's default checked out commit (the auto-merge, IIRC)?

[Damiano Testa]

Eric, maybe I am not understanding your comment, but the action contains a script that should be run both on master and on the PR branch, in order to measure the changes to the import graph.

[Eric Wieser]

I claim you should be checking out GITHUB_SHA not $BRANCH_NAME. The latter doesn't include the latest master.

[Damiano Testa]

On the topic of the file name, this has been changed and you can see #21699 for what happens with the change.

EDIT: the bot reaction is simply a test that I was trying out! :smile:

[Damiano Testa]

Eric, I am going to look up the differences between the two commits (I am not sure that I even knew that there was a difference) and will report back!

[Eric Wieser]

GITHUB_SHA is the result of merging master into BRANCH_NAME, roughly

[Damiano Testa]

I see, so you are saying that GITHUB_SHA will have a smaller diff with master than BRANCH_NAME and hence the PR summary will have an easier starting point, right?

[Eric Wieser]

More that it will be more likely to be using an up to date version of the shell script