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

[via Digitalmars-d-bugs]

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

Vladimir Panteleev <thecybershadow at gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|ASSIGNED                    |RESOLVED
         Resolution|---                         |WORKSFORME

--- Comment #9 from Vladimir Panteleev <thecybershadow at gmail.com> ---
GitHub PR interface has improved a lot since this issue was opened (labels,
checklists, filtering etc.), so I think we can now close this.

--