| author | hoelzl | 
| Thu, 09 Jun 2011 14:24:34 +0200 | |
| changeset 43342 | 2929f96d3ae7 | 
| parent 35022 | c844b93dd147 | 
| permissions | -rwxr-xr-x | 
| 26575 | 1 | #!/usr/bin/env bash | 
| 2 | # | |
| 3 | # Author: Makarius | |
| 4 | # | |
| 5 | # DESCRIPTION: simple XML to YXML converter | |
| 6 | ||
| 7 | ||
| 8 | PRG="$(basename "$0")" | |
| 9 | ||
| 10 | function usage() | |
| 11 | {
 | |
| 12 | echo | |
| 28650 | 13 | echo "Usage: isabelle $PRG" | 
| 26575 | 14 | echo | 
| 15 | echo " Convert XML (stdin) to YXML (stdout)." | |
| 16 | echo | |
| 17 | exit 1 | |
| 18 | } | |
| 19 | ||
| 20 | function fail() | |
| 21 | {
 | |
| 22 | echo "$1" >&2 | |
| 23 | exit 2 | |
| 24 | } | |
| 25 | ||
| 26 | ||
| 27 | ## process command line | |
| 28 | ||
| 29 | [ "$#" -ne 0 ] && usage | |
| 30 | ||
| 31 | ||
| 32 | ## main | |
| 33 | ||
| 35022 
c844b93dd147
modernized perl scripts: prefer standalone executables;
 wenzelm parents: 
29143diff
changeset | 34 | exec "$ISABELLE_HOME/lib/scripts/yxml" |