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;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # DESCRIPTION: translate symbols into \<...> sequences
     8 
     9 #set by configure
    10 AUTO_PERL=perl
    11 
    12 exec "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/symbolinput.pl" "$@"