diff options
Diffstat (limited to 'doc')
-rw-r--r-- | doc/Makefile | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/Makefile b/doc/Makefile index 871dd431d..3cc89b059 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -32,7 +32,6 @@ pdf: guide.pdf features.pdf clean: rm -f *.aux rm -f *.haux - rm -f *.html rm -f *.htoc rm -f *.idx rm -f *.ilg @@ -41,7 +40,10 @@ clean: rm -f *.out rm -f *.pdf rm -f *.toc - rm contributed_modules.tex + [ ! -f contributed_modules.tex ] || rm contributed_modules.tex + +distclean: clean + rm -f *.html guide.html: guide.tex hevea -fix -pedantic guide.tex |