Pushed as ee79286031..bd511903de to master.

--
Oleg