File jedit-installer.patch of Package jedit

--- jEdit/./installer/OperatingSystem.java~	2004-01-27 23:11:59.000000000 -0500
+++ jEdit/installer/OperatingSystem.java	2004-01-27 23:12:44.000000000 -0500
@@ -147,46 +147,6 @@
 			public void perform(String installDir,
 				Vector filesets) throws IOException
 			{
-				if(!enabled)
-					return;
-
-				mkdirs(directory);
-
-				String name = installer.getProperty("app.name");
-
-				// create app start script
-				String script = directory + File.separatorChar
-					+ name.toLowerCase();
-
-				// Delete existing copy
-				new File(script).delete();
-
-				// Write simple script
-				FileWriter out = new FileWriter(script);
-				out.write("#!/bin/sh\n");
-				out.write("# Java heap size, in megabytes\n");
-				out.write("JAVA_HEAP_SIZE=32\n");
-				out.write("DEFAULT_JAVA_HOME=\""
-					+ System.getProperty("java.home")
-					+ "\"\n");
-				out.write("if [ \"$JAVA_HOME\" = \"\" ]; then\n");
-				out.write("JAVA_HOME=\"$DEFAULT_JAVA_HOME\"\n");
-				out.write("fi\n");
-
-				out.write("exec \"$JAVA_HOME"
-					+ "/bin/java\" -mx${JAVA_HEAP_SIZE}m ${"
-					+ name.toUpperCase() + "} ");
-
-				String jar = installDir + File.separator
-					+ name.toLowerCase() + ".jar";
-
-				out.write("-jar \"" + jar + "\" $@\n");
-
-				out.close();
-
-				// Make it executable
-				String[] chmodArgs = { "chmod", "755", script };
-				exec(chmodArgs);
 			}
 		}