Source builds randomly fail at doc generation

[Péter Szilágyi]

Hey all,

  I'm using gmplib to cross compile to various platforms and architectures
(10-15) builds, one after the other, and every now and again (maybe every
20th) my `make` fails with an error that `makeinfo` command cannot be
found. If I restart the exact same build it will complete successfully. As
far as I've noticed it's platform/configuration independent. I know that I
could just as well install texinfo, and that's indeed one solution, but it
requires an extra configuration step on my build servers which I'd like to
avoid if possible.

  This issue only appeared with the switch to 6.1.0. I've been running the
previous 6.0.0a release for a very long time and seen no failures like this
one.

Cheers,
  Peter

PS: If it matters, I'm cross compiling from Linux (Ubuntu 15.10) to
Linux/Windows/OSX/Android/iOS arm/i386/amd64. There is no pattern in which
of those builds fail and when, it just happens randomly.