Re: [PATCH] [RFC] gdb: add disable-docs option

[Mike Frysinger <vapier@gentoo.org>]

[-- Attachment #1: Type: text/plain, Size: 998 bytes --]

On 06 Sep 2015 11:37, Romain Naour wrote:
> If makeinfo is not found in the system then the missing
> script is used to warn the user.
> 
> Before commit e30465112ed4c6320dd19107302057a5f7712cf2 the missing
> script returned 0 after printing the message.
> 
> Now, missing return 127 (command not found) to the Makefile and
> the build fail.
> 
> As suggested [1], add a new option to disable the documentation.

aren't info pages shipped as part of the release ?  so even if makeinfo isn't
available, it doesn't matter as the pages aren't regenerated on the user's
system.  maybe you're applying patches to the source that cause the docs to be
regenerated ?  if that's the case, i think disabling the docs entirely is the
wrong way to go.  instead it should be skipping the regeneration step and
installing the pages that already exist.  alternatively, you can adjust your
build to update the timestamps of the generated files so the build won't try
to regenerate them.
-mike

[-- Attachment #2: Digital signature --]
[-- Type: application/pgp-signature, Size: 819 bytes --]