lib/Tools/symbolinput
changeset 9788 df671fa2562a
parent 6082 590f9e3bf4d8
child 10555 2323ec838401
     1.1 --- a/lib/Tools/symbolinput	Fri Sep 01 17:48:31 2000 +0200
     1.2 +++ b/lib/Tools/symbolinput	Fri Sep 01 17:50:36 2000 +0200
     1.3 @@ -1,10 +1,12 @@
     1.4  #!/bin/bash
     1.5  #
     1.6  # $Id$
     1.7 +# Author: Markus Wenzel, TU Muenchen
     1.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  #
    1.10  # DESCRIPTION: translate symbols into \<...> sequences
    1.11  
    1.12  #set by configure
    1.13  AUTO_PERL=perl
    1.14  
    1.15 -exec $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
    1.16 +exec "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/symbolinput.pl" "$@"