Clean up *.pla files -- platform annotation information.

diff --git a/Doc/tools/mkhowto.sh b/Doc/tools/mkhowto.sh
index 373430d3779ad2499e1d8aa9aa9a3c792bc7787e..76bbda6555ea8582184ab73a0178027f798414dd 100755 (executable)
--- a/Doc/tools/mkhowto.sh
+++ b/Doc/tools/mkhowto.sh
@@ -165,7 +165,7 @@ l2hoption() {
 }
 
 cleanup() {
-    rm -f $1.aux $1.log $1.out $1.toc $1.bkm $1.idx $1.ilg $1.ind $1.syn
+    rm -f $1.aux $1.log $1.out $1.toc $1.bkm $1.idx $1.ilg $1.ind $1.syn $1.pla
     rm -f mod$1.idx mod$1.ilg mod$1.ind
     if [ ! "$BUILD_DVI" ] ; then
        rm -f $1.dvi