Huh, yes, they appear to have coincidentally fixed it since I wrote that comment. Maybe I need to start reporting all GitHub bugs as Hacker News comments...