On Sun, Dec 11, 2016 at 03:03:08PM -0500, Leo Famulari wrote:
> On Sun, Dec 11, 2016 at 02:30:33PM -0500, Mark H Weaver wrote:
> > ludo@gnu.org (Ludovic Courtès) writes:
> > > I’d be in favor of merging now though.
> > >
> > > What do people think?
> > 
> > Sounds fine to me.
> 
> Okay, shall I go ahead and do it?

And, pushed as 4a990395d749619c6e565c57a05c0ca9f6894eed

Thanks everyone!