On Wed, Nov 25, 2015 at 5:43 AM, Pádraig Brady <[email protected]> wrote:
> On 25/11/15 12:53, Joachim Schiele wrote:
>> i've used this patch but then i hit this issue:
>> http://paste.ubuntu.com/13498376/
>>
>> i don't have packaged makeinfo yet and i don't really care for the
>> documentation at the moment. i didn't find a ./configure switch to
>> disable it either.
>
>> and there is a patch to make it compile without
>> 'makeinfo' which changes doc/local.mk but it seems already applied in
>> 8.24 so what should i do now?
>
> I don't know what patch you're referring to, but
> it would be best to avoid makeinfo unless really needed.
> The attached should do that (note you may want to
> apply it to Makefile.in rather than doc/local.mk,
> and note it requires cmp on the build system).
Good idea.
- && mv $@-t $@
+ && { cmp -s $@-t $@ 2>/dev/null || mv $@-t $@; }
That "-s" option works with GNU cmp, but is not portable to some
other-vendor cmp programs.
