# HG changeset patch
# User wenzelm
# Date 1275909605 -7200
# Node ID 1255ba99ed1e6381c0546e515963783753440230
# Parent  865ad5634ed87afffd53e2b82daf0cb4c55b633e
no symlinks;
tuned;

diff -r 865ad5634ed8 -r 1255ba99ed1e src/Tools/jEdit/makedist
--- a/src/Tools/jEdit/makedist	Mon Jun 07 11:42:54 2010 +0200
+++ b/src/Tools/jEdit/makedist	Mon Jun 07 13:20:05 2010 +0200
@@ -11,7 +11,7 @@
 
 ## diagnostics
 
-JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre17"
+JEDIT_HOME=""
 
 function usage()
 {
@@ -20,7 +20,6 @@
   echo
   echo "  Options are:"
   echo "    -j DIR       specify original jEdit distribution"
-  echo "                 (default: $JEDIT_HOME)"
   echo
   echo "  Produce Isabelle/jEdit distribution from Netbeans build"
   echo "  in $THIS/dist"
@@ -66,12 +65,13 @@
 
 # target name
 
+[ -z "$JEDIT_HOME" ] && fail "Unknown JEDIT_HOME"
+
 VERSION=$(basename "$JEDIT_HOME")
 JEDIT="jedit-${VERSION}"
 
 rm -rf "$JEDIT" jedit
 mkdir "$JEDIT"
-ln -s "$JEDIT" jedit
 
 
 # copy stuff
@@ -95,5 +95,4 @@
 # build archive
 
 echo "${JEDIT}.tar.gz"
-tar czf "${JEDIT}.tar.gz" "$JEDIT" jedit
-ln -sf "${JEDIT}.tar.gz" jedit.tar.gz
+tar czf "${JEDIT}.tar.gz" "$JEDIT"