lib/Tools/symbolinput
author wenzelm
Tue Apr 22 11:37:12 1997 +0200 (1997-04-22)
changeset 3007 e5efa177ee0c
parent 2589 9d910f3681d0
child 4508 f102cb0140fe
permissions -rwxr-xr-x
removed -norc;
wenzelm@3007
     1
#!/bin/bash
wenzelm@2399
     2
#
wenzelm@2399
     3
# $Id$
wenzelm@2399
     4
#
wenzelm@2399
     5
# DESCRIPTION: translate symbols into \<...> sequences
wenzelm@2399
     6
#
wenzelm@2589
     7
# NOTE: If perl is unavailable we simply fall back on ucat!
wenzelm@2399
     8
wenzelm@2399
     9
wenzelm@2399
    10
PERL=$(type -path perl)
wenzelm@2399
    11
wenzelm@2399
    12
if [ -z "$PERL" ]
wenzelm@2399
    13
then
wenzelm@2589
    14
  exec $ISABELLE_HOME/lib/scripts/ucat "$@"
wenzelm@2399
    15
else
wenzelm@2399
    16
  exec $PERL $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
wenzelm@2399
    17
fi