Ralf Wildenhues wrote: > Thanks for the report. OK to push this patch, tested 'make info pdf > html'? You forgot "dvi". cheers, DaveK