DrJava Legacy SVN Repository

#!/bin/sh

if [[ -z "${JAVA_HOME}" ]]; then
    echo "Error: JAVA_HOME must be set"

fi

if [[ -z "${HJ_HOME}" ]]; then
    echo "Error: HJ_HOME must be set"
    exit 1
else
	rm -Rf input/*.jar
	cp ${HJ_HOME}/lib/*.jar misc/drjava-hj/input
fi

if [[ -z "${JAVA5_HOME}" ]]; then
    export JAVA5_HOME=${JAVA_HOME}
fi

cd drjava
ant clean jar
cd ../misc/drjava-hj
rm *.jar
cp ../../drjava/drjava.jar .
ant clean drjava-hj
echo "A new jar has been created in misc/drjava-hj/"