symbolinput - translate symbols into \<...> sequences;
authorwenzelm
Mon Dec 16 09:58:16 1996 +0100 (1996-12-16)
changeset 23996719b465198b
parent 2398 d4164ea87229
child 2400 4b08766bc9d1
symbolinput - translate symbols into \<...> sequences;
lib/Tools/symbolinput
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/Tools/symbolinput	Mon Dec 16 09:58:16 1996 +0100
     1.3 @@ -0,0 +1,17 @@
     1.4 +#!/bin/bash -norc
     1.5 +#
     1.6 +# $Id$
     1.7 +#
     1.8 +# DESCRIPTION: translate symbols into \<...> sequences
     1.9 +#
    1.10 +# NOTE: If perl is unavailable we simply fall back on cat!
    1.11 +
    1.12 +
    1.13 +PERL=$(type -path perl)
    1.14 +
    1.15 +if [ -z "$PERL" ]
    1.16 +then
    1.17 +  exec cat "$@"
    1.18 +else
    1.19 +  exec $PERL $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
    1.20 +fi