diff options
Diffstat (limited to 'doc/user')
| -rw-r--r-- | doc/user/Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/user/Makefile b/doc/user/Makefile index b8947ef60f..cbbc2e3e95 100644 --- a/doc/user/Makefile +++ b/doc/user/Makefile @@ -59,7 +59,7 @@ html: dirs $(FILES) $(PROJECT).texi clean: - rm -f *.o $(PROG) *.txt core *.html *.pdf + rm -f *.o $(PROG) *.txt core *.html $(PROJECT).pdf rm -f *.dvi *.ps *.log *.aux *.cp *.fn *.ky *.pg *.toc *.tp *.vr $(BASE) rm -f c_user c_user-* _* $(GENERATED_FILES) @@ -185,3 +185,4 @@ mp.texi: mp.t convert: /usr/bin/gs -dMaxBitmap=300000000 -g5500x5500 -sDEVICE=pdfwrite -q -dNOPAUSE -dSAFER -sOutputFile=rtemspie.pdf -- rtemspie.eps -c -quit + /usr/bin/gs -dMaxBitmap=300000000 -g5500x5500 -sDEVICE=pdfwrite -q -dNOPAUSE -dSAFER -sOutputFile=states.pdf -- states.eps -c -quit |