CI issue with #14174

Stream: mathlib4

[Kevin Buzzard]

What did I do wrong with #14174 ? The PR clarifies a docstring but it's failed CI. The error is

Run PR="14174"
Previous HEAD position was 01a942001f Merge ea87a47615bdd7569618ee9fe75d86ab8f770a6f into cf35070bb02a05a6405bf8b62238aeacf0583ea0
Switched to a new branch 'kbuzzard-sections-docstring'
branch 'kbuzzard-sections-docstring' set up to track 'origin/kbuzzard-sections-docstring'.
/home/runner/work/_temp/42d7a8fe-d069-49d0-8864-0d9d4a102b94.sh: line 27: ./scripts/update_PR_comment.sh: No such file or directory
Error: Process completed with exit code 127.

[Ruben Van de Velde]

You started the branch from a three-week-old master

[Ruben Van de Velde]

Merge master and I expect it will be fine