author | wenzelm |
Wed, 04 Oct 2000 20:55:57 +0200 | |
changeset 10150 | a068c666c53e |
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" "$@" |