src/Tools/jEdit/makedist
changeset 37355 1255ba99ed1e
parent 37218 ffd587207d5d
child 41513 0ffd5ea44078
--- 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"