lib/Tools/symbolinput
author wenzelm
Fri, 07 Mar 1997 11:48:46 +0100
changeset 2754 59bd96046ad6
parent 2589 9d910f3681d0
child 3007 e5efa177ee0c
permissions -rwxr-xr-x
moved settings comment to build;
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
#
2589
9d910f3681d0 now falls back on ucat instead of cat;
wenzelm
parents: 2399
diff changeset
     7
# NOTE: If perl is unavailable we simply fall back on ucat!
2399
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
2589
9d910f3681d0 now falls back on ucat instead of cat;
wenzelm
parents: 2399
diff changeset
    14
  exec $ISABELLE_HOME/lib/scripts/ucat "$@"
2399
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