lib/Tools/install
author wenzelm
Fri, 01 Sep 2000 17:50:36 +0200
changeset 9788 df671fa2562a
parent 7934 42836b6c4c73
child 10030 950580516dfa
permissions -rwxr-xr-x
GPLed; more robust handling of spaces in args / file names;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     1
#!/bin/bash
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     2
#
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     3
# $Id$
9788
wenzelm
parents: 7934
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm
parents: 7934
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     6
#
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
     7
# DESCRIPTION: install standalone Isabelle executables
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     8
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     9
9788
wenzelm
parents: 7934
diff changeset
    10
PRG=$(basename "$0")
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    11
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    12
function usage()
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    13
{
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    14
  echo
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    15
  echo "Usage: $PRG [OPTIONS]"
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    16
  echo
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    17
  echo "  Options are:"
7887
eedfff88ee40 tuned usage;
wenzelm
parents: 6545
diff changeset
    18
  echo "    -d DISTDIR   refer to DISTDIR as Isabelle distribution"
eedfff88ee40 tuned usage;
wenzelm
parents: 6545
diff changeset
    19
  echo "                 (default ISABELLE_HOME)"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    20
  echo "    -k           install KDE application icon on Desktop"
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    21
  echo "    -p DIR       install standalone binaries in DIR"
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    22
  echo
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    23
  echo "  Install Isabelle executables with absolute references to the current"
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    24
  echo "  distribution directory."
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    25
  echo
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    26
  exit 1
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    27
}
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    28
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    29
function fail()
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    30
{
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    31
  echo "$1" >&2
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    32
  exit 2
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    33
}
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    34
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    35
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    36
## process command line
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    37
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    38
# options
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    39
6450
990e6e2dee26 improved usage;
wenzelm
parents: 6417
diff changeset
    40
NO_OPTS=true
990e6e2dee26 improved usage;
wenzelm
parents: 6417
diff changeset
    41
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    42
DISTDIR="$ISABELLE_HOME"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    43
KDE=""
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    44
BINDIR=""
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    45
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    46
while getopts "d:kp:" OPT
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    47
do
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    48
  case "$OPT" in
5404
wenzelm
parents: 5403
diff changeset
    49
    d)
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    50
      DISTDIR="$OPTARG"
6450
990e6e2dee26 improved usage;
wenzelm
parents: 6417
diff changeset
    51
      NO_OPTS=""
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    52
      ;;
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    53
    k)
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    54
      KDE=true
6450
990e6e2dee26 improved usage;
wenzelm
parents: 6417
diff changeset
    55
      NO_OPTS=""
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    56
      ;;
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    57
    p)
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    58
      BINDIR="$OPTARG"
6450
990e6e2dee26 improved usage;
wenzelm
parents: 6417
diff changeset
    59
      NO_OPTS=""
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    60
      ;;
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    61
    \?)
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    62
      usage
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    63
      ;;
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    64
  esac
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    65
done
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    66
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    67
shift $(($OPTIND - 1))
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    68
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    69
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    70
# args
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    71
9788
wenzelm
parents: 7934
diff changeset
    72
[ "$#" -ne 0 -o -n "$NO_OPTS" ] && usage
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    73
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    74
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    75
## main
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    76
6459
1d13a86bfa6c fixed ISABELLE_HOME/lib/logo/isabelle-tiny.xpm;
wenzelm
parents: 6450
diff changeset
    77
echo "referring to distribution at $DISTDIR"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    78
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    79
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    80
# standalone binaries
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    81
6082
590f9e3bf4d8 configure AUTO_BASH, AUTO_PERL;
wenzelm
parents: 5404
diff changeset
    82
#set by configure
590f9e3bf4d8 configure AUTO_BASH, AUTO_PERL;
wenzelm
parents: 5404
diff changeset
    83
AUTO_BASH=/bin/bash
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    84
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    85
if [ -n "$BINDIR" ]; then
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    86
  mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    87
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    88
  for NAME in isatool isabelle Isabelle
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    89
  do
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    90
    BIN="$BINDIR/$NAME"
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    91
    DIST="$DISTDIR/bin/$NAME"
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    92
    echo "installing $BIN"
9788
wenzelm
parents: 7934
diff changeset
    93
    echo "#!$AUTO_BASH" > "$BIN" || fail "Cannot write file: $BIN"
wenzelm
parents: 7934
diff changeset
    94
    echo >> "$BIN"
wenzelm
parents: 7934
diff changeset
    95
    echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
wenzelm
parents: 7934
diff changeset
    96
    chmod +x "$BIN"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    97
  done
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    98
fi
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
    99
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
   100
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
   101
# install KDE application icon
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
   102
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
   103
KDEHOME=~/.kde
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
   104
KDEAPP=~/Desktop/Isabelle.kdelnk
9788
wenzelm
parents: 7934
diff changeset
   105
KDEICONS="$KDEHOME/share/icons"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
   106
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
   107
if [ "$KDE" = true ]; then
9788
wenzelm
parents: 7934
diff changeset
   108
  mkdir -p "$KDEICONS" || fail "Bad directory: $KDEICONS"
wenzelm
parents: 7934
diff changeset
   109
  mkdir -p "$KDEICONS/mini" || fail "Bad directory: $KDEICONS/mini"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
   110
9788
wenzelm
parents: 7934
diff changeset
   111
  [ -f "$KDEICONS/isabelle.xpm" ] || cp "$ISABELLE_HOME/lib/icons/isabelle.xpm" "$KDEICONS" || \
6545
a8a235a8a4a3 improved icons;
wenzelm
parents: 6459
diff changeset
   112
    fail "Cannot write file: $KDEICONS/isabelle.xpm"
9788
wenzelm
parents: 7934
diff changeset
   113
  [ -f "$KDEICONS/mini/isabelle.xpm" ] || \
wenzelm
parents: 7934
diff changeset
   114
    cp "$ISABELLE_HOME/lib/icons/isabelle-mini.xpm" "$KDEICONS/mini/isabelle.xpm" || \
6545
a8a235a8a4a3 improved icons;
wenzelm
parents: 6459
diff changeset
   115
    fail "Cannot write file: $KDEICONS/mini/isabelle.xpm"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
   116
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
   117
  echo "installing $KDEAPP"
9788
wenzelm
parents: 7934
diff changeset
   118
  echo "# KDE Config File" > "$KDEAPP" || fail "Cannot write file: $KDEAPP"
wenzelm
parents: 7934
diff changeset
   119
  echo "[KDE Desktop Entry]" >> "$KDEAPP"
wenzelm
parents: 7934
diff changeset
   120
  echo "Type=Application" >> "$KDEAPP"
wenzelm
parents: 7934
diff changeset
   121
  echo "Exec=$DISTDIR/bin/Isabelle %f" >> "$KDEAPP"
wenzelm
parents: 7934
diff changeset
   122
  echo "Icon=isabelle.xpm" >> "$KDEAPP"
wenzelm
parents: 7934
diff changeset
   123
  echo "TerminalOptions=" >> "$KDEAPP"
wenzelm
parents: 7934
diff changeset
   124
  echo "Path=" >> "$KDEAPP"
wenzelm
parents: 7934
diff changeset
   125
  echo "Terminal=0" >> "$KDEAPP"
wenzelm
parents: 7934
diff changeset
   126
  echo "Name=Isabelle" >> "$KDEAPP"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
   127
9788
wenzelm
parents: 7934
diff changeset
   128
  echo "Please refresh your KDE now!"
6417
39941b906910 -p option;
wenzelm
parents: 6082
diff changeset
   129
fi