2020-05-22 UTC
# 
[dmitshur] not worth spending time on that particular page. I'm moving in the direction of not depending on GitHub at all on most pages. this is one of the few cases where there's some dependence on GH, and it will eventually be obsolete anyway.