diff options
Diffstat (limited to 'Doc/tools/mkhowto.sh')
| -rwxr-xr-x | Doc/tools/mkhowto.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Doc/tools/mkhowto.sh b/Doc/tools/mkhowto.sh index fa1a8c2..6ba4869 100755 --- a/Doc/tools/mkhowto.sh +++ b/Doc/tools/mkhowto.sh @@ -127,7 +127,7 @@ build_ps() { } cleanup() { - rm -f $1.aux $1.log $1.out $1.toc $1.bkm $1.idx $1.ind + rm -f $1.aux $1.log $1.out $1.toc $1.bkm $1.idx $1.ind mod$1.ind if [ ! "$BUILD_DVI" ] ; then rm -f $FILE.dvi fi |