Subject: Re: bug#9597: update

From: Dima Kogan <[email-masked]>
Date: Wed, 25 Jan 2017 14:16:11 -0800

Can we please merge this? It fixes a long-standing and annoying bug that
we KNOW exists, and has NO side-effects that we know about. If issues
pop up, we can deal with them.

I can push this, just need the green light.