lib/Tools/symbolinput
author wenzelm
Thu Nov 30 20:10:29 2000 +0100 (2000-11-30)
changeset 10555 2323ec838401
parent 9788 df671fa2562a
permissions -rwxr-xr-x
/usr/bin/env bash;
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@2399
     2
#
wenzelm@2399
     3
# $Id$
wenzelm@9788
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@9788
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@2399
     6
#
wenzelm@2399
     7
# DESCRIPTION: translate symbols into \<...> sequences
wenzelm@2399
     8
wenzelm@6082
     9
#set by configure
wenzelm@6082
    10
AUTO_PERL=perl
wenzelm@6082
    11
wenzelm@9788
    12
exec "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/symbolinput.pl" "$@"