src/Tools/jEdit/makedist

--- a/src/Tools/jEdit/makedist	Mon May 31 21:29:27 2010 +0200
+++ b/src/Tools/jEdit/makedist	Mon May 31 22:08:40 2010 +0200
@@ -84,6 +84,7 @@
 cp -R jars/. "$JEDIT/jars/."
 
 cp -R "$THIS/dist-template/." "$JEDIT/."
+cp "$THIS/README" "$JEDIT/."
 
 perl -i -e 'while (<>) { if (m/NAME="javacc"/) {
   print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;