wok diff ecj/stuff/ecj.sh.part @ rev 23169

updated mediainfo (19.04 -> 19.09)
author Hans-G?nter Theisgen
date Wed Mar 18 09:07:11 2020 +0100 (2020-03-18)
parents
children
line diff
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/ecj/stuff/ecj.sh.part	Wed Mar 18 09:07:11 2020 +0100
     1.3 @@ -0,0 +1,23 @@
     1.4 +
     1.5 +if [ -n "$ECJ_VERSION" ] ; then
     1.6 +	ECJ_JAR="ecj-$ECJ_VERSION.jar"
     1.7 +else
     1.8 +	ECJ_JAR="ecj.jar"
     1.9 +fi
    1.10 +
    1.11 +if [ -z "$JAVA" ] ; then
    1.12 +	if [ -n "$(which java)" ] ; then
    1.13 +		JAVA=java
    1.14 +	elif [ -n "$(which jamvm)" ] ; then
    1.15 +		JAVA=jamvm
    1.16 +	elif [ -n "$(which gij)" ] ; then
    1.17 +		JAVA=gij
    1.18 +	elif [ -n "$(which kaffe)" ] ; then
    1.19 +		JAVA=kaffe
    1.20 +	else
    1.21 +		echo "Java interpreter not found"
    1.22 +		exit 1
    1.23 +	fi
    1.24 +fi
    1.25 +
    1.26 +$JAVA -cp /usr/share/java/$ECJ_JAR  org.eclipse.jdt.internal.compiler.batch.Main "$@"