[Issue 12254] Github interaction improvement proposals (via user.js or addins)

[via Digitalmars-d-bugs]

https://issues.dlang.org/show_bug.cgi?id=12254

--- Comment #10 from Andrej Mitrovic <andrej.mitrovich at gmail.com> ---
> you can't filter through closed pulls where you can tell whether a pull was closed because it was merged, or it was closed but not merged.

I think this one is still true.

But otherwise yeah things have improved. :)

--