lib/Tools/logo
changeset 5557 d6ceb4275742
child 5570 ae1b56ef16b0
equal deleted inserted replaced
5556:28e12dc85d29 5557:d6ceb4275742
       
     1 #!/bin/bash
       
     2 #
       
     3 # $Id$
       
     4 #
       
     5 # DESCRIPTION: create an instance of the Isabelle logo
       
     6 
       
     7 
       
     8 PRG=$(basename $0)
       
     9 
       
    10 function usage()
       
    11 {
       
    12   echo
       
    13   echo "Usage: $PRG NAME"
       
    14   echo
       
    15   echo "  Create instance NAME of the Isabelle logo (as EPS to stdout)."
       
    16   echo
       
    17   exit 1
       
    18 }
       
    19 
       
    20 function fail()
       
    21 {
       
    22   echo "$1" >&2
       
    23   exit 2
       
    24 }
       
    25 
       
    26 
       
    27 ## args
       
    28 
       
    29 NAME=""
       
    30 [ $# -ge 1 ] && { NAME="$1"; shift; }
       
    31 
       
    32 [ $# -ne 0 -o "$NAME" = "-?" -o -z "$NAME" ] && usage
       
    33 
       
    34 
       
    35 ## main
       
    36 
       
    37 perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps