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