Subject: Re: zsh manual - missing bookmarks in pdf file?
From: Peter Stephenson <[email-masked]>
To: "[email-masked]" <[email-masked]>
Date: Fri, 04 Mar 2016 15:08:52 +0000
List-Id: Zsh Workers List <zsh-workers.zsh.org>

On Fri, 4 Mar 2016 23:25:40 +0900
Jun T. <[email-masked]> wrote:
> The patch includes a possible fix for this, but is it really
> necessary to check for pdfetex? Since texi2dvi checks for
> pdfetex by itself, probably PDFTEX=$(PDFETEX) is not necessary.
> Or it may be there for a (very) old texi2dvi?

It probably was originally there for older versions of texi2dvi, but
that doesn't mean it's necessarily still needed.  We have prepackaged
documentation for systems that can't keep up with tools.

pws