Always use --dvips-safe when generating HTML for the standard documentation
since we do not have anything that causes dvips to be run except when
PostScript is specifically requested, which is a separate target.
1 file changed