author | wenzelm |
Thu, 20 Mar 1997 11:38:58 +0100 | |
changeset 2827 | cce436a62740 |
parent 2589 | 9d910f3681d0 |
child 3007 | e5efa177ee0c |
permissions | -rwxr-xr-x |
#!/bin/bash -norc # # $Id$ # # DESCRIPTION: translate symbols into \<...> sequences # # NOTE: If perl is unavailable we simply fall back on ucat! PERL=$(type -path perl) if [ -z "$PERL" ] then exec $ISABELLE_HOME/lib/scripts/ucat "$@" else exec $PERL $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@" fi