Generate PDF and convert it to PS instead of generating DVI,
converting DVI to PS and then converting PS to PDF.

TODO: Can we use pdfjadetex instead of `jadetex -output-format=pdf'?
TODO: Last $(JADETEX) invocation should not have a leading `-'.

Index: doc.docbook.dsssl.mk
===================================================================
RCS file: /cvsroot/htdocs/share/mk/doc.docbook.dsssl.mk,v
retrieving revision 1.11
diff -u -p -r1.11 doc.docbook.dsssl.mk
--- doc.docbook.dsssl.mk	13 Oct 2005 09:24:33 -0000	1.11
+++ doc.docbook.dsssl.mk	18 Feb 2019 18:30:22 -0000
@@ -106,15 +106,14 @@ ${DOC}.html: ${DOC}.xml
 .xml.tex:
 	${JADE} ${JADE_OPTS} ${DSL_TEX_OPTS} -o $@ $(XML_DECL) $<
 
-.tex.ps:
-	-$(JADETEX) $*.tex
-	-$(JADETEX) $*.tex
-	-$(JADETEX) $*.tex
-	${DVIPS} -f $*.dvi > $@
+.tex.pdf:
+	-$(JADETEX) -output-format=pdf $*.tex
+	-$(JADETEX) -output-format=pdf $*.tex
+	-$(JADETEX) -output-format=pdf $*.tex
 	rm -f *.log *.aux
 
-.ps.pdf:
-	$(PS2PDF) $<
+.pdf.ps:
+	$(PDF2PS) $<
 
 # w3m doesn't render &#8220 or &#8221 properly, so just replace them
 # with normal double quotes.
Index: doc.docbook.mk
===================================================================
RCS file: /cvsroot/htdocs/share/mk/doc.docbook.mk,v
retrieving revision 1.29
diff -u -p -r1.29 doc.docbook.mk
--- doc.docbook.mk	19 Feb 2017 23:15:10 -0000	1.29
+++ doc.docbook.mk	18 Feb 2019 18:30:22 -0000
@@ -117,8 +117,7 @@ SX_ENCODING?=	iso-8859-1
 SED?=		/usr/bin/sed
 CAT?=		/bin/cat
 
-PS2PDF?=	${PREFIX}/bin/ps2pdf
-DVIPS?=		${PREFIX}/bin/dvips
+PDF2PS?=	${PREFIX}/bin/pdf2ps
 
 W3M_BIN?=	${PREFIX}/bin/w3m
 W3M_OPTS=	-dump ${XML_ENCODING:S/^/-O /} -no-graph ${W3M_FLAGS}	
@@ -146,7 +145,7 @@ CLEANFILES+=	${SXERR}
 
 .MAIN: all
 
-all pdf html html-split ascii: build
+all ps html html-split ascii: build
 
 .if make(html)
 FORMATS?=	html