# HG changeset patch # User wenzelm # Date 1224618469 -7200 # Node ID 545a73fee0e31fba7c86801670f5502ce00cecae # Parent 2cb3369f0634b4127d417dbec1e4c01e0edf6303 make Isabelle/jEdit distribution; diff -r 2cb3369f0634 -r 545a73fee0e3 src/Tools/jEdit/makedist --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/makedist Tue Oct 21 21:47:49 2008 +0200 @@ -0,0 +1,102 @@ +#!/usr/bin/env bash +# +# makedist -- make Isabelle/jEdit distribution + +## self references + +PRG=$(basename "$0") +THIS=$(cd "$(dirname "$0")"; pwd) +SUPER=$(cd "$THIS/.."; pwd) + + +## diagnostics + +JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre15" +SCALA_HOME="/home/scala/current" + +function usage() +{ + echo + echo "Usage: $PRG [OPTIONS]" + echo + echo " Options are:" + echo " -j DIR specify original jEdit distribution" + echo " (default: $JEDIT_HOME)" + echo " -s DIR specify Scala distribution" + echo " (default: $SCALA_HOME)" + echo + echo " Produce Isabelle/jEdit distribution from Netbeans build" + echo " in $THIS/dist" + echo + exit 1 +} + +fail() +{ + echo "$1" >&2 + exit 2 +} + + +## process command line + +# options + +while getopts "j:s:" OPT +do + case "$OPT" in + j) + JEDIT_HOME="$OPTARG" + ;; + s) + SCALA_HOME="$OPTARG" + ;; + \?) + usage + ;; + esac +done + +shift $(($OPTIND - 1)) + + +# args + +[ "$#" -ne 0 ] && usage + + +## main + +cd "$THIS/dist" || fail "Bad directory: $THIS/dist" + + +# target name + +VERSION=$(basename "$JEDIT_HOME") +JEDIT="jedit-${VERSION}" + +rm -rf "$JEDIT" jedit +mkdir "$JEDIT" +ln -s "$JEDIT" jedit + + +# copy stuff + +[ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME" +cp -R "$JEDIT_HOME/." "$JEDIT/." + +[ "$SCALA_HOME/lib/scala-library.jar" ] || fail "Bad Scala directory: $SCALA_HOME" +cp "$SCALA_HOME/lib/scala-library.jar" "$JEDIT/jars/" + +cp -R "$THIS/dist-template/." "$JEDIT/." + +cp Isabelle-jEdit.jar "$JEDIT/jars/isabelle.jar" +cp lib/Pure.jar "$JEDIT/jars/isabelle-Pure.jar" +cp lib/core-renderer.jar "$JEDIT/jars/" + + +# build archive + +echo "${JEDIT}.tar.gz" +tar czf "${JEDIT}.tar.gz" "$JEDIT" jedit +ln -sf "${JEDIT}.tar.gz" jedit.tar.gz