obsolete, cf. build.xml and makedist;
authorwenzelm
Sat, 20 Dec 2008 13:27:48 +0100
changeset 34416 283a974972b4
parent 34415 3f76ce248c0e
child 34417 bce2f2ea9819
obsolete, cf. build.xml and makedist;
src/Tools/jEdit/plugin/IsabellePlugin.ant
--- a/src/Tools/jEdit/plugin/IsabellePlugin.ant	Sat Dec 20 12:32:40 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-<?xml version="1.0"?>
-<project name="IsabellePlugin installer" default="install" basedir=".">
-  <target name="install">
-  	<copy file="services.xml" todir="bin" />
-  	<copy file="dockables.xml" todir="bin" />
-  	<copy file="actions.xml" todir="bin" />
-  	<copy file="IsabellePlugin.props" todir="bin" />
-    <jar destfile="IsabellePlugin.jar" basedir="bin" /> 
-  </target>
-</project>
\ No newline at end of file