I committed a fix.

On Thu, Oct 26, 2017 at 5:18 PM, Policeman Jenkins Server
<[EMAIL PROTECTED]> wrote: