diff --git a/build.sh b/build.sh index 39eeb1062147922e1219d2c73fe57e38d613b680..ee2f195a65cc26d21a16f6a3681d538af977d9a6 100755 --- a/build.sh +++ b/build.sh @@ -457,6 +457,8 @@ distclean() rm -rf 3rdparty || failure rm -rf build || failure rm -rf install || failure + rm -rf doc/html || failure + rm -f doc/*.tag || failure rm -f .lastbuild || failure }