lib/Tools/symbolinput
author wenzelm
Fri Sep 01 17:50:36 2000 +0200 (2000-09-01)
changeset 9788 df671fa2562a
parent 6082 590f9e3bf4d8
child 10555 2323ec838401
permissions -rwxr-xr-x
GPLed;
more robust handling of spaces in args / file names;
wenzelm@3007
     1
#!/bin/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" "$@"