| changeset 2399 | 6719b465198b |
| child 2589 | 9d910f3681d0 |
| 2398:d4164ea87229 | 2399:6719b465198b |
|---|---|
1 #!/bin/bash -norc |
|
2 # |
|
3 # $Id$ |
|
4 # |
|
5 # DESCRIPTION: translate symbols into \<...> sequences |
|
6 # |
|
7 # NOTE: If perl is unavailable we simply fall back on cat! |
|
8 |
|
9 |
|
10 PERL=$(type -path perl) |
|
11 |
|
12 if [ -z "$PERL" ] |
|
13 then |
|
14 exec cat "$@" |
|
15 else |
|
16 exec $PERL $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@" |
|
17 fi |