From f49eb01498548ece4ba4844a9d0727c45dd6d4e3 Mon Sep 17 00:00:00 2001 From: Taylor R Campbell Date: Fri, 16 Aug 2019 02:51:41 +0000 Subject: [PATCH] Produce 300dpi, not 72dpi, PNGs for HTML output. --- doc/make-common.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/make-common.in b/doc/make-common.in index bcf004cc2..7a7504e04 100644 --- a/doc/make-common.in +++ b/doc/make-common.in @@ -77,7 +77,7 @@ PS_TARGET = $(TARGET_ROOT).ps GS = gs PS2PDF = ps2pdf -PS2PNG = $(GS) -dSAFER -dBATCH -dNOPAUSE -sDEVICE=png16m +PS2PNG = $(GS) -dSAFER -dBATCH -dNOPAUSE -sDEVICE=png16m -r300 TEX_OPTIONS = --quiet $(EXTRA_TEX_OPTIONS) -- 2.25.1