update_PR_comment.sh: No such file or directory

Stream: mathlib4

[Haocheng Wang]

Hi, I am currently working on the PR of the Auction Theory but failed to solve this error message. In the one last push this kind of error didn't occur. I am really curious how can I solve this problem.

Run PR="13248"
Previous HEAD position was 31fe328853 Merge df87fef06fd491b1b0298a1764c247e95b4a8289 into bdd39e92aed38bcac548ae0859ba269c95dbc2f2
Switched to a new branch 'gametheory-auction-secondprice'
branch 'gametheory-auction-secondprice' set up to track 'origin/gametheory-auction-secondprice'.
/home/runner/work/_temp/bfbe5675-838a-4c50-b89d-707ba53ee1cd.sh: line 27: ./scripts/update_PR_comment.sh: No such file or directory
Error: Process completed with exit code 127.

feat: basic concepts of game theory · leanprover-community/mathlib4@df87fef (github.com)
My branch is as below.
leanprover-community/mathlib4 at gametheory-auction-secondprice (github.com)

[Yaël Dillies]

You need to merge master

[Haocheng Wang]

\

[Haocheng Wang]

Yaël Dillies said:

You need to merge master

Hi Yaël, does that mean I can not left the commits behind the master branch? Or my branch need to be merged to the master.

[Yaël Dillies]

None of your options are idiomatic in git-speak, but I believe the correct one is the first

[Yaël Dillies]

Do something like git fetch, git merge origin/master