prose_lint.py Keeps the Tab Git Appends to a Header Whose Path Holds a Space, So That File Leaves Scope

[ptr727]

Problem

Git appends a literal tab to a +++ header whose path contains a space, to mark where the path ends. diff_header_path in .github/actions/prose-gate/prose_lint.py never strips it, so such a file silently leaves diff scope.

Both quoting states are affected, by different routes:

• Unquoted. The header is +++ b/with space.md<TAB>, so the key becomes with space.md<TAB>, which matches no discovered file.
• Quoted, where the name also holds a byte at or above 0x80. The header is +++ "b/one two.md"<TAB>, so the field does not end in a quote, the unquoting branch never fires, the field does not begin b/, and the file is dropped outright.

Either way the scope ends up empty, and an empty scope is falsy, so the if scope and not matched refusal in main never fires and the run exits 0.

Evidence

Constructed: a repository whose only change adds a duplicated word to a file whose name contains a space.

--diff HEAD    scope: 0 of 1 file(s) read     exit 0
whole tree     the violation reported         exit 1

Confirmed present at a3cd9c7, so this is not a regression from #1574. The new TestDiffScopeReachesAQuotedName does not cover it, since no name in its table contains a space.

Reach

Any repository holding a path with a space in it, which is ordinary in a docs tree. The gate reports clean on every such file in diff mode, which is the mode the action always runs.

Suggested fix

The tab is a terminator rather than part of the path, so strip at the first tab before deciding whether the field is quoted. Add a name holding a space, and one holding both a space and a non-ASCII character, to the table in TestDiffScopeReachesAQuotedName.

Found by a local review pass while fixing #1538 in #1574.