lib/Tools/symbolinput

added -g, -h options;
replaced ISABELLE_HTML by ISABELLE_USEDIR_OPTIONS;

#!/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