diff options
Diffstat (limited to 'Makefile.in')
| -rw-r--r-- | Makefile.in | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/Makefile.in b/Makefile.in index f55642388..f454cbd1a 100644 --- a/Makefile.in +++ b/Makefile.in @@ -76,9 +76,13 @@ environment: @echo " done" man: man/ptxdist.1.gz -man/ptxdist.1.gz: doc/ptxdist.man doc/ref_parameter.inc +man/ptxdist.1: doc/ptxdist.man doc/ref_parameter.inc @mkdir -pv man - $(RST2MAN) $< 2>/dev/null | gzip > $@ + $(RST2MAN) $< $@ + +.INTERMEDIATE: man/ptxdist.1 +man/ptxdist.1.gz: man/ptxdist.1 + gzip $< clean: @rm -f .done |