1
#!/bin/bash
2
#
3
# $Id$
4
5
# DESCRIPTION: translate symbols into \<...> sequences
6
7
#set by configure
8
AUTO_PERL=perl
9
10
exec $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"