author | wenzelm |
Thu, 24 Sep 1998 21:32:12 +0200 | |
changeset 5557 | d6ceb4275742 |
child 5570 | ae1b56ef16b0 |
permissions | -rwxr-xr-x |
#!/bin/bash # # $Id$ # # DESCRIPTION: create an instance of the Isabelle logo PRG=$(basename $0) function usage() { echo echo "Usage: $PRG NAME" echo echo " Create instance NAME of the Isabelle logo (as EPS to stdout)." echo exit 1 } function fail() { echo "$1" >&2 exit 2 } ## args NAME="" [ $# -ge 1 ] && { NAME="$1"; shift; } [ $# -ne 0 -o "$NAME" = "-?" -o -z "$NAME" ] && usage ## main perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps