1 files changed, 0 insertions, 3 deletions
diff --git a/build.xml b/build.xml
index e8bd5179e7..c83ad41f1e 100755
--- a/build.xml
+++ b/build.xml
@@ -1723,9 +1723,6 @@ TODO:
     <copy                            toDir="${dist.dir}/doc/licenses" overwrite="true">
       <fileset dir="${docs.dir}/licenses"/>
     </copy>
-    <copy                            toDir="${dist.dir}/doc/tools" overwrite="true">
-      <fileset dir="${build-docs.dir}/manual/html"/>
-    </copy>
 
     <mkdir dir="${dist.dir}/api"/>
     <copy toDir="${dist.dir}/api" overwrite="true">