Produce 300dpi, not 72dpi, PNGs for HTML output.

diff --git a/doc/make-common.in b/doc/make-common.in
index bcf004cc20c637556f4fa019b543d29fbf920cc9..7a7504e0452a0487634ac166d0cc1fde801a08c9 100644 (file)
--- 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)