From 153c71043f6b039ad5c28c41d711456e280f0ad5 Mon Sep 17 00:00:00 2001
From: Lukas Ladenberger <lukas.ladenberger@googlemail.com>
Date: Thu, 26 Apr 2012 09:51:17 +0000
Subject: [PATCH] removed building plugin zip file from build script (migrated
 to gradle)

git-svn-id: svn://svn.code.sf.net/p/rodin-b-sharp/svn/trunk/Handbook@14616 1434b563-b632-4741-aa49-43a3a8374d2e
---
 org.rodinp.handbook.feature/customBuild.xml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/org.rodinp.handbook.feature/customBuild.xml b/org.rodinp.handbook.feature/customBuild.xml
index 9ddec43..6b4daef 100644
--- a/org.rodinp.handbook.feature/customBuild.xml
+++ b/org.rodinp.handbook.feature/customBuild.xml
@@ -1,7 +1,8 @@
 <project default="generate-all">
 
 	<property name="build-dir" value="${basedir}/build"/>
-	
+	<!--${eclipse.workspace}
+	${workspace_loc}-->
 	<property name="theme-html" value="rodin-theme-html"/>
 	<property name="theme-eclipse" value="rodin-theme-eclipse"/>	
 	
@@ -58,7 +59,7 @@
     	  <replacevalue><![CDATA[<toc topic="index.html" ]]></replacevalue>
         </replace>
     	
-    	<!-- delete old eclipse help zip -->
+    	<!-- delete old eclipse help zip x
     	<delete dir="${build-dir}/plugin" includes="*.zip"/>
     	
     	<tstamp>
@@ -74,6 +75,8 @@
     	       update="true" />
     
     	<delete dir="${build-dir}/plugin/plugins"/>
+		-->
+    	
     </target>
 
     <target name="generate" depends="init">
@@ -94,8 +97,7 @@
     	<replaceregexp
     		match="plasTeX.Base.LaTeX.Index.IndexDestination[^>]*"
     		replace="plasTeX.Base.LaTeX.Index.IndexDestination/"
-    		flags="g"
-    	>
+    		flags="g">
     		<fileset dir="${targetdir}" includes="*.html"/>
     	</replaceregexp>
     </target>
-- 
GitLab