From d68bbe4b832d1a44473577d0dc004523a8ca6d3a Mon Sep 17 00:00:00 2001
From: Adriaan Moors <adriaan.moors@typesafe.com>
Date: Fri, 13 Dec 2013 12:36:15 -0800
Subject: Fixup for #3265

---
 build.xml | 3 ---
 1 file changed, 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">
-- 
cgit v1.2.3