lib/scripts/feeder
changeset 9789 7e5e6c47c0b5
parent 6082 590f9e3bf4d8
child 10512 d34192966cd8
equal deleted inserted replaced
9788:df671fa2562a 9789:7e5e6c47c0b5
     1 #!/bin/bash
     1 #!/bin/bash
     2 #
     2 #
     3 # $Id$
     3 # $Id$
       
     4 # Author: Markus Wenzel, TU Muenchen
       
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     4 #
     6 #
     5 # feeder - feed isabelle session
     7 # feeder - feed isabelle session
     6 
     8 
     7 
     9 
     8 ## diagnostics
    10 ## diagnostics
     9 
    11 
    10 PRG=$(basename $0)
    12 PRG=$(basename "$0")
    11 DIR=$(dirname $0)
    13 DIR=$(dirname "$0")
    12 
    14 
    13 function usage()
    15 function usage()
    14 {
    16 {
    15   echo
    17   echo
    16   echo "Usage: $PRG [OPTIONS]"
    18   echo "Usage: $PRG [OPTIONS]"
    71 shift $(($OPTIND - 1))
    73 shift $(($OPTIND - 1))
    72 
    74 
    73 
    75 
    74 # args
    76 # args
    75 
    77 
    76 [ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
    78 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
    77 
    79 
    78 
    80 
    79 
    81 
    80 ## main
    82 ## main
    81 
    83 
    82 #set by configure
    84 #set by configure
    83 AUTO_PERL=perl
    85 AUTO_PERL=perl
    84 
    86 
    85 exec $AUTO_PERL -w $DIR/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"
    87 exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"