Can we please kill the hyphenator already?

[Jonathan M Davis]

On Monday, September 30, 2013 00:29:20 Dicebot wrote:
> On Sunday, 29 September 2013 at 22:25:03 UTC, H. S. Teoh wrote:
> > Wait, didn't somebody already merge the pull to kill off the
> > hyphenator?

Yes, I merged it.

> Did web-site actually get updated since that pull?

I don't think so. IIRC, it's just Andrei and Walter who have permissions to do 
that, and it only normally happens when there's a release. Occasionally Andrei 
will update it after certain pulls, but since he didn't merge this one, he 
didn't update the site afterwards (and AFAIK, he hasn't updated the site for 
any other pulls).

- Jonathan M Davis