On 10/04/2018 01:17 PM, Aleksey Shipilev wrote: >> Ok to push? > > OK. Please note the configuration name change: it is not linux-x86_64-normal-server-fastdebug anymore, it is linux-x86_64-server-fastdebug. Better purge the old configuration, so you don't use that accidentally. -Aleksey