equal
deleted
inserted
replaced
1 #!/bin/bash |
1 #!/bin/bash |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
|
4 # Author: Markus Wenzel, TU Muenchen |
|
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 # |
6 # |
5 # DESCRIPTION: create an instance of the Isabelle logo |
7 # DESCRIPTION: create an instance of the Isabelle logo |
6 |
8 |
7 |
9 |
8 PRG=$(basename $0) |
10 PRG=$(basename "$0") |
9 |
11 |
10 function usage() |
12 function usage() |
11 { |
13 { |
12 echo |
14 echo |
13 echo "Usage: $PRG [OPTIONS] NAME" |
15 echo "Usage: $PRG [OPTIONS] NAME" |
54 |
56 |
55 |
57 |
56 # args |
58 # args |
57 |
59 |
58 NAME="-" |
60 NAME="-" |
59 [ $# -ge 1 ] && { NAME="$1"; shift; } |
61 [ "$#" -ge 1 ] && { NAME="$1"; shift; } |
60 |
62 |
61 [ $# -ne 0 -o "$NAME" = "-" ] && usage |
63 [ "$#" -ne 0 -o "$NAME" = "-" ] && usage |
62 |
64 |
63 |
65 |
64 ## main |
66 ## main |
65 |
67 |
66 if [ -z "$OUTFILE" ]; then |
68 if [ -z "$OUTFILE" ]; then |
71 |
73 |
72 #set by configure |
74 #set by configure |
73 AUTO_PERL=perl |
75 AUTO_PERL=perl |
74 |
76 |
75 if [ "$OUTFILE" = "-" ]; then |
77 if [ "$OUTFILE" = "-" ]; then |
76 $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps |
78 "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" |
77 else |
79 else |
78 [ -z "$QUIET" ] && echo "$OUTFILE" >&2 |
80 [ -z "$QUIET" ] && echo "$OUTFILE" >&2 |
79 $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE |
81 "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTFILE" |
80 fi |
82 fi |