info() {
  echo "INFO: $1"
}