Enable/Disable proxy settings defined elsewhere

proxy

#!/bin/bash
# Toggle proxy settings.
# It will be necessary to reload ${HOME}/.profile after running this.

USAGE="usage: ${0} on|off|status"

if [[ "d${PROXY_FILE}d" == "dd" ]]; then
  echo "PROXY_FILE undefined" >&2
  exit 1
fi

if [[ $# -ne 1 ]]; then
  echo ${USAGE} >&2
  exit 1
elif [[ "$1" == "status" ]]; then
  if [[ -f "${PROXY_FILE}" ]]; then
    echo "proxy ON"
  else
    echo "proxy OFF"
  fi
elif [[ "$1" == "on" ]]; then
  touch ${PROXY_FILE}
elif [[ "$1" == "off" ]]; then
  if [[ -f ${PROXY_FILE} ]]; then
    rm -f ${PROXY_FILE}
  fi
else
  echo ${USAGE} >&2
  exit 1
fi