--- a/lib/scripts/feeder Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/feeder Fri Sep 01 17:54:58 2000 +0200
@@ -1,14 +1,16 @@
#!/bin/bash
#
# $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# feeder - feed isabelle session
## diagnostics
-PRG=$(basename $0)
-DIR=$(dirname $0)
+PRG=$(basename "$0")
+DIR=$(dirname "$0")
function usage()
{
@@ -73,7 +75,7 @@
# args
-[ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
+[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
@@ -82,4 +84,4 @@
#set by configure
AUTO_PERL=perl
-exec $AUTO_PERL -w $DIR/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"
+exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"