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