lib/Tools/install
author wenzelm
Sat, 21 Nov 1998 12:17:18 +0100
changeset 5944 dcc446da8e19
parent 5404 fde117f1006b
child 6082 590f9e3bf4d8
permissions -rwxr-xr-x
added undos, redos;
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$
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     4
#
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
     5
# DESCRIPTION: install binaries with absolute references to distribution
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     6
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     7
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     8
PRG=$(basename $0)
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
     9
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    10
function usage()
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
  echo
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    13
  echo "Usage: $PRG BINDIR"
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    14
  echo
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    15
  echo "  Options are:"
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    16
  echo "    -d DISTDIR   use DISTDIR as Isabelle distribution (default ISABELLE_HOME)"
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    17
  echo
5404
wenzelm
parents: 5403
diff changeset
    18
  echo "  Install standalone Isabelle binaries in directory BINDIR with absolute"
wenzelm
parents: 5403
diff changeset
    19
  echo "  references to DISTDIR/bin, which becomes non-relocatable this way."
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    20
  echo
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    21
  exit 1
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    22
}
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    23
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    24
function fail()
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    25
{
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    26
  echo "$1" >&2
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    27
  exit 2
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
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    30
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    31
## process command line
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    32
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    33
# options
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    34
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    35
DISTDIR="$ISABELLE_HOME"
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    36
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    37
while getopts "d:" OPT
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    38
do
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    39
  case "$OPT" in
5404
wenzelm
parents: 5403
diff changeset
    40
    d)
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    41
      DISTDIR="$OPTARG"
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    42
      ;;
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    43
    \?)
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    44
      usage
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    45
      ;;
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    46
  esac
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    47
done
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    48
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    49
shift $(($OPTIND - 1))
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    50
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    51
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    52
# args
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    53
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    54
BINDIR=""
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    55
[ $# -ge 1 ] && { BINDIR="$1"; shift; }
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    56
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    57
[ $# -ne 0 -o -z "$BINDIR" -o "$BINDIR" = "-?" ] && usage
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    58
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    59
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    60
## main
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    61
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    62
mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    63
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    64
BASH=$(type -path bash)
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    65
[ -z "$BASH" ] && fail "Cannot find bash!"
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
echo "using $DISTDIR"
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    68
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    69
for NAME in isatool isabelle Isabelle
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    70
do
5403
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    71
  BIN="$BINDIR/$NAME"
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    72
  DIST="$DISTDIR/bin/$NAME"
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    73
  echo "installing $BIN"
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    74
  echo "#!$BASH" >$BIN || fail "Cannot write file: $BIN"
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    75
  echo >>$BIN
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    76
  echo "exec $DIST \"\$@\"" >>$BIN
aa04ac8bfeae -d DISTDIR;
wenzelm
parents: 5398
diff changeset
    77
  chmod +x $BIN
5362
29ce4f1fe72c install binaries with absolute references to ISABELLE_HOME/bin;
wenzelm
parents:
diff changeset
    78
done