From 80b5d4524431069a5f13edb900f8e9e6a6bfbb90 Mon Sep 17 00:00:00 2001
From: Oliver Bock <oliver.bock@aei.mpg.de>
Date: Fri, 11 Jul 2008 15:48:21 +0200
Subject: [PATCH] Added doc related files/folders to distclean target

---
 build.sh | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/build.sh b/build.sh
index 39eeb10..ee2f195 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
 }
-- 
GitLab