Open KoviRobi opened 8 years ago
The workaround we use in Jenkins is to build with MAKEINFO=missing in the environment of configure and make. This causes the documentation make targets to be disabled.
You can also use cheribuild.py binutils
from https://github.com/RichardsonAlex/cheri-scripts which will automatically set all the required flags like MAKEINFO=missing and also forcing -std=gnu89
You get an error like:
This is just the documentation failing to compile. A hack is to run this before
make
:This works because it updates the timestamps on the documentation, so that
make
will not build it.(Putting this here as a workaround, should somebody else also encounter this. Sorry if it is the wrong place for this.)