lib/scripts/feeder

Correction of a tiny error

#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# feeder - feed isabelle session


## diagnostics

PRG="$(basename "$0")"
DIR="$(dirname "$0")"

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS]"
  echo
  echo "  Options are:"
  echo "    -h TEXT      head text"
  echo "    -p           emit my pid"
  echo "    -q           do not pipe stdin"
  echo "    -t TEXT      tail text"
  echo
  echo "  Output texts (pid, head, stdin, tail), then wait to be terminated."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

HEAD=""
EMITPID=""
QUIT=""
TAIL=""

while getopts "h:pqt:" OPT
do
  case "$OPT" in
    h)
      HEAD="$OPTARG"
      ;;
    p)
      EMITPID=true
      ;;
    q)
      QUIT=true
      ;;
    t)
      TAIL="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }



## main

exec perl -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"