On Friday, 26 January 2018 at 20:43:05 UTC, Fra Mecca wrote:
What should I do now? I am undecided between: - commenting on the bug tracker and close the bug - link the pr 6056 on the bug tracker - leaving it be
Leaving a comment on the bug with a link to the PR, and marking the bug resolved fixed is exactly what you should do, and thank you. :)
-- Simen
