--- a/lib/Tools/logo Tue Mar 09 14:20:27 2021 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,77 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: create an instance of the Isabelle logo (PDF)
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS] [XYZ]"
- echo
- echo " Create instance XYZ of the Isabelle logo (PDF)."
- echo
- echo " Options are:"
- echo " -o FILE alternative output file (default \"isabelle_xyx.pdf\")"
- echo " -q quiet mode"
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-# options
-
-OUTPUT_FILE=""
-QUIET=""
-
-while getopts "o:q" OPT
-do
- case "$OPT" in
- o)
- OUTPUT_FILE="$OPTARG"
- ;;
- q)
- QUIET=true
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-TEXT=""
-[ "$#" -ge 1 ] && { TEXT="$1"; shift; }
-
-[ "$#" -ne 0 ] && usage
-
-
-## main
-
-if [ -z "$OUTPUT_FILE" ]; then
- OUTPUT_NAME="$(echo "$TEXT" | tr A-Z a-z)"
- if [ -z "$OUTPUT_NAME" ]; then
- OUTPUT_FILE="isabelle.pdf"
- else
- OUTPUT_FILE="isabelle_${OUTPUT_NAME}.pdf"
- fi
-fi
-
-[ -z "$QUIET" ] && echo "$OUTPUT_FILE" >&2
-perl -p -e "s,<any>,$TEXT," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" | \
- "$ISABELLE_EPSTOPDF" --filter > "$OUTPUT_FILE"