Converting the http_proxy environment variable to Java settings via script

Since this involves some shell parameter expansion magic, here is a very simple script for copying the "http_proxy" environment variable to the Java proxy properties:

if [ -n "$http_proxy" ]; then
  # http_proxy should be something like http://host:port
  # trim the "http://" off:
  local host="${http_proxy#http://}"
  # trim the host part off:
  local port="${host#*:}"
  # The final substitution removes the port for the host,
  # and removes any (erroneously) appended junk to the port.
  JAVA_OPTS="$JAVA_OPTS -Dhttp.proxyHost=${host%:*}\
    -Dhttp.proxyPort=${port%/*}"
fi

The JAVA_OPTS variable will now have the proxy settings appended to it.