lib/Tools/symbolinput
author paulson
Thu, 23 Jan 1997 10:35:28 +0100
changeset 2538 c55f68761a8d
parent 2399 6719b465198b
child 2589 9d910f3681d0
permissions -rwxr-xr-x
Mended spelling error
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2399
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     1
#!/bin/bash -norc
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     2
#
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     3
# $Id$
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     4
#
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: translate symbols into \<...> sequences
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     6
#
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     7
# NOTE: If perl is unavailable we simply fall back on cat!
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     8
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     9
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
    10
PERL=$(type -path perl)
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
    11
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
    12
if [ -z "$PERL" ]
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
    13
then
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
    14
  exec cat "$@"
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
    15
else
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
    16
  exec $PERL $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
    17
fi