On Mon, Jan 16, 2017 at 04:25:36PM +0100, Tobias Geerinckx-Rice wrote:
> On 15/01/17 20:06, Leo Famulari wrote:
> > If the latter, I think we should instead pass '--disable-mutool'
> 
> This is fine by me. Done and thrown in the push queue.

Okay, can you send the patch to the list, so that anyone who might be
using mutool has a good chance to comment?