lean/batteries pr comment script fails

Stream: mathlib4

[Edward van de Meent]

the script for adding comments to lean and batteries PRs saying whether mathlib builds, now errors. presumably since #15996 was merged. See for example this run.

[Edward van de Meent]

(I guess somewhat curiously, the CI still appropriately changes the label, it just doesn't add a comment saying something along the lines of "CI succeeded at [insert date]")

[Edward van de Meent]

the issue is a typo: in the action, the variable COUNTEREXAMPLE_OUTCOME is set, while the actual script expects COUNTEREXAMPLES_OUTCOME

[Edward van de Meent]

should i change the script or the action?

[Damiano Testa]

I would use Counterexamples since that is the name of the repo.

[Edward van de Meent]

right, i'll make a PR updating the actions then (i read the doc comments, so ill be using mk_build_yml.sh, no worries)

[Bryan Gin-ge Chen]

Aha! I guess the action was just silently ignoring the output of the script before #15996 made it stricter. Thanks for noticing and fixing this!

[Edward van de Meent]

PR at #18617

[Edward van de Meent]

:tada: the fix worked