On Thu Dec 14 23:56:01 2017, marka wrote:
> It should be good to commit.

=> merged to master, v9_12, v9_11, v9_10 and v9_9.