diff --git a/src/script/ant b/src/script/ant index 87858e865..a97c5c97b 100644 --- a/src/script/ant +++ b/src/script/ant @@ -44,11 +44,18 @@ if $no_config ; then rpm_mode=false usejikes=$use_jikes_default else + orig_ant_home=$ANT_HOME # load system-wide ant configuration if [ -f "/etc/ant.conf" ] ; then . /etc/ant.conf fi + # Normally users do not expect that /etc/ant.conf will override ANT_HOME + if [ -n "$orig_ant_home" -a "$orig_ant_home" != "$ANT_HOME" ] ; then + echo "Warning: ANT_HOME has been overridden by /etc/ant.conf from $orig_ant_home to $ANT_HOME" + echo " Use ant -noconfig if this is not desired." + fi + # load user ant configuration if [ -f "$HOME/.ant/ant.conf" ] ; then . $HOME/.ant/ant.conf