| changeset 12456 | 95bed2b95448 |
| parent 12455 | 7633c0fad9bd |
| child 12457 | cbfc53e45476 |
| 12455:7633c0fad9bd | 12456:95bed2b95448 |
|---|---|
1 #!/usr/bin/env 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" "$@" |