lib/Tools/yxml
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 35022 c844b93dd147
permissions -rwxr-xr-x
updated for release;
     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
    13   echo "Usage: isabelle $PRG"
    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 
    34 exec "$ISABELLE_HOME/lib/scripts/yxml"