# HG changeset patch
# User wenzelm
# Date 906665532 -7200
# Node ID d6ceb4275742ffa14b026ea8600690e378fa7375
# Parent  28e12dc85d298f5d5ed52656b26620a1ba75737b
create an instance of the Isabelle logo;

diff -r 28e12dc85d29 -r d6ceb4275742 lib/Tools/logo
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/logo	Thu Sep 24 21:32:12 1998 +0200
@@ -0,0 +1,37 @@
+#!/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