#!/bin/bash -norc## $Id$## DESCRIPTION: translate symbols into \<...> sequences## NOTE: If perl is unavailable we simply fall back on cat!PERL=$(type -path perl)if [ -z "$PERL" ]then exec cat "$@"else exec $PERL $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"fi