lib/scripts/ucat
author wenzelm
Mon, 16 Dec 1996 10:29:30 +0100
changeset 2411 256dbda3df4f
parent 2347 a42c1b835fb3
child 2579 4af1023fc6bf
permissions -rwxr-xr-x
SML/NJ startup script (for 0.93).
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2347
a42c1b835fb3 added -norc option;
wenzelm
parents: 2307
diff changeset
     1
#!/bin/bash -norc
2306
0aadfaf8557a ucat - uninterruptible cat
wenzelm
parents:
diff changeset
     2
#
2307
508d2a233dbc *** empty log message ***
wenzelm
parents: 2306
diff changeset
     3
# $Id$
508d2a233dbc *** empty log message ***
wenzelm
parents: 2306
diff changeset
     4
#
2347
a42c1b835fb3 added -norc option;
wenzelm
parents: 2307
diff changeset
     5
# ucat - uninterruptible cat.
2307
508d2a233dbc *** empty log message ***
wenzelm
parents: 2306
diff changeset
     6
#
2306
0aadfaf8557a ucat - uninterruptible cat
wenzelm
parents:
diff changeset
     7
# NOTE: If perl is unavailable we simply fall back on normal cat!
2307
508d2a233dbc *** empty log message ***
wenzelm
parents: 2306
diff changeset
     8
2306
0aadfaf8557a ucat - uninterruptible cat
wenzelm
parents:
diff changeset
     9
0aadfaf8557a ucat - uninterruptible cat
wenzelm
parents:
diff changeset
    10
PERL=$(type -path perl)
0aadfaf8557a ucat - uninterruptible cat
wenzelm
parents:
diff changeset
    11
0aadfaf8557a ucat - uninterruptible cat
wenzelm
parents:
diff changeset
    12
if [ -z "$PERL" ]
0aadfaf8557a ucat - uninterruptible cat
wenzelm
parents:
diff changeset
    13
then
0aadfaf8557a ucat - uninterruptible cat
wenzelm
parents:
diff changeset
    14
  exec cat "$@"
0aadfaf8557a ucat - uninterruptible cat
wenzelm
parents:
diff changeset
    15
else
0aadfaf8557a ucat - uninterruptible cat
wenzelm
parents:
diff changeset
    16
  exec $PERL -e '$SIG{INT} = "IGNORE"; $| = 1; while (<ARGV>) {print;}' "$@"
0aadfaf8557a ucat - uninterruptible cat
wenzelm
parents:
diff changeset
    17
fi