On 2014/11/16 15:27, Yozo Toda wrote: > -----BEGIN PGP SIGNED MESSAGE----- > Hash: SHA512 > > Dear sthen, chrisz, > > > >http://junkpile.org/coq.log > > > > > >I'm not sure why this has broken now, the port hasn't changed for a > > >while. > > >Might be picking up something (texlive? hevea?) in configure.. > > I'll try to check tonight the relevant Makefile of coq > (which is generated by configure). > > Quick look at my log when I built coq-8.4pl4 about two weeks ago, > I found the difference in the output of configure > > ] latex was not found; documentation will not be available > > I always compiled coq without latex, because texlive is > a very huge size package. > > sthen, your building environment is changed recently? > Anyway, generated Makefile should be consistent with configure.
Thanks. So, the build environment is constantly changing. DPB is installing and uninstalling packages all the time during a build, so if there is some optional dependency that may be picked up by configure, it either must be listed as a dependency in the port's Makefile, or the configure check needs to be disabled (either by a command-line option, environment variable, or patching if necessary). Looks like in this case adding "--with-doc=no" should do the trick.
