ci: remove the false pipefail comment that reached main

[Abdk4Moura]

A comment asserting a bug that does not exist is on main, and I put it there.

My retraction commit did not land before #128 was squashed, so the merge carried the pre-retraction state. I merged it myself without re-checking that the force-push had arrived. That is exactly what I said I would least like to ship, inside a PR about false claims.

What the comment claimed, and why it is wrong

It said shell: bash runs bash -e without pipefail. The reverse is true:

shell: bash              ->  bash --noprofile --norc -eo pipefail {0}
no shell key (default)   ->  bash -e {0}

The explicit form, which reads like a no-op, is the one that adds pipefail. This step has it. So the macOS harness pipe never swallowed cargo's status, and those greens were always valid evidence — for #83, #113, #118, #119 and #122.

The now-redundant set -o pipefail goes with the comment. In its place: a note recording which form supplies pipefail and that a commit briefly claimed the opposite, so the next reader inherits the correction rather than repeating the inference. Refuted by claude-advisor and verified against GitHub's own workflow-syntax documentation before writing this.

What stays

#128's warning-ratchet fixes are untouched and remain real, because neither depends on pipefail:

• cargo check ... | grep "^warning:" > file || true explicitly discards the status, so a tree that does not compile still scores zero warnings and passes the ratchet.
• A missing .github/warning-baseline became 9999, a ceiling nothing could exceed, silently turning the gate off.

That step has no shell: key, so it genuinely runs the bare default without pipefail, and its set -o pipefail is correct and stays.

Process note

Verify a force-push landed before merging a PR you amended. gh pr merge will squash whatever the remote actually holds, not what your local branch says. The amend and the merge were minutes apart and I checked neither.