# 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"