diff options
| -rw-r--r-- | doc/Makefile | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/Makefile b/doc/Makefile index 64f6f434de..b306018624 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -36,6 +36,7 @@ clean: ./do_docs $(BASEDIR) clean cd tools/bmenu ; gmake clean cd tools/pdl2texi ; gmake clean + cd tools/src2html ; gmake clean .PHONY: tools @@ -43,3 +44,4 @@ clean: tools: cd tools/bmenu ; gmake cd tools/pdl2texi ; gmake + cd tools/src2html ; gmake |