| changeset 26575 | 042617a1c86c |
| child 28650 | a7ba12e0d3b7 |
| 26574:560d07845442 | 26575:042617a1c86c |
|---|---|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # $Id$ |
|
4 # Author: Makarius |
|
5 # |
|
6 # DESCRIPTION: simple XML to YXML converter |
|
7 |
|
8 |
|
9 PRG="$(basename "$0")" |
|
10 |
|
11 function usage() |
|
12 { |
|
13 echo |
|
14 echo "Usage: $PRG" |
|
15 echo |
|
16 echo " Convert XML (stdin) to YXML (stdout)." |
|
17 echo |
|
18 exit 1 |
|
19 } |
|
20 |
|
21 function fail() |
|
22 { |
|
23 echo "$1" >&2 |
|
24 exit 2 |
|
25 } |
|
26 |
|
27 |
|
28 ## process command line |
|
29 |
|
30 [ "$#" -ne 0 ] && usage |
|
31 |
|
32 |
|
33 ## main |
|
34 |
|
35 exec perl -w "$ISABELLE_HOME/lib/scripts/yxml.pl" |