On Tue, Sep 11, 2018 at 07:33:36AM +0800, Alex Vong wrote:
> Jonathan Brielmaier <jonathan.brielmaier@web.de> writes:
> > Somehow the commit message didn't reflect what was done there. Should be
> > "Update to 2018.09.08" :)
> 
> You're right, I forget to change the commit message. But it has been
> pushed, what should we do now?

Nothing :)

It was a mistake and we documented it here. There's nothing left to do
to fix it.