Is makeinfo required?

[pierre-24]

Even though I do not want to build the documentation (because I'm using your library in a CI context, inside a docker container), I still need to install texinfo, otherwise I get

WARNING: 'makeinfo' is missing on your system.
You should only need it if you modified a '.texi' file, or
any other file indirectly affecting the aspect of the manual.
You might want to install the Texinfo package:
http://www.gnu.org/software/texinfo/
The spurious makeinfo call might also be the consequence of
using a buggy 'make' (AIX, DU, IRIX), in which case you might
want to install GNU make:
http://www.gnu.org/software/make/

while running

autoreconf -i
./configure
make  # ! this fails

Not that I cannot install texinfo, but the TeX distribution is >1Gio, and I would like to keep the docker image as light as possible (I currently include texiinfo, but if I can get rid of it, that would be nice)

Thanks in advance :)

[brarcher]

There is now a configure flag which controls if docs are built. See #212 for details. If that is not sufficient, please re-open.