lib/Tools/install
changeset 5404 fde117f1006b
parent 5403 aa04ac8bfeae
child 6082 590f9e3bf4d8
equal deleted inserted replaced
5403:aa04ac8bfeae 5404:fde117f1006b
    13   echo "Usage: $PRG BINDIR"
    13   echo "Usage: $PRG BINDIR"
    14   echo
    14   echo
    15   echo "  Options are:"
    15   echo "  Options are:"
    16   echo "    -d DISTDIR   use DISTDIR as Isabelle distribution (default ISABELLE_HOME)"
    16   echo "    -d DISTDIR   use DISTDIR as Isabelle distribution (default ISABELLE_HOME)"
    17   echo
    17   echo
    18   echo "  Install binaries in directory BINDIR with absolute references to"
    18   echo "  Install standalone Isabelle binaries in directory BINDIR with absolute"
    19   echo "  DISTDIR/bin, which basically becomes non-relocatable this way."
    19   echo "  references to DISTDIR/bin, which becomes non-relocatable this way."
    20   echo
    20   echo
    21   exit 1
    21   exit 1
    22 }
    22 }
    23 
    23 
    24 function fail()
    24 function fail()
    35 DISTDIR="$ISABELLE_HOME"
    35 DISTDIR="$ISABELLE_HOME"
    36 
    36 
    37 while getopts "d:" OPT
    37 while getopts "d:" OPT
    38 do
    38 do
    39   case "$OPT" in
    39   case "$OPT" in
    40     h)
    40     d)
    41       DISTDIR="$OPTARG"
    41       DISTDIR="$OPTARG"
    42       ;;
    42       ;;
    43     \?)
    43     \?)
    44       usage
    44       usage
    45       ;;
    45       ;;