Re: Make doc failing

[Graham Percival]

On Sat, Jul 30, 2011 at 09:26:04PM -0600, Carl Sorensen wrote:
> For the past while, I've had to run make doc more than once to get it to
> succeed.  I've been unable to track down the problem, but since multiple
> runs fixes it, I haven't worried too much about it.

That's not reliable; make doc can skip over a file that failed in
the previous build.

IMO, any build which passes
  ../configure
but fails the first run of
  make
  make doc
is a Critical issue.  This is not yet an official policy, but I
hope to make it so as soon as we discuss the "Issues priorities"
item.  (having logs for build-system output will help immensely,
of course!)

Cheers,
- Graham