lib/Tools/version
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 48837 d1d806a42c91
child 67865 ab0b8e388967
permissions -rwxr-xr-x
updated for release;
berghofe@13804
     1
#!/usr/bin/env bash
berghofe@13804
     2
#
berghofe@13804
     3
# Author: Stefan Berghofer, TU Muenchen
wenzelm@41511
     4
# Author: Makarius
berghofe@13804
     5
#
berghofe@13804
     6
# DESCRIPTION: display Isabelle version
berghofe@13804
     7
wenzelm@41511
     8
wenzelm@41511
     9
PRG="$(basename "$0")"
wenzelm@41511
    10
wenzelm@41511
    11
function usage()
wenzelm@41511
    12
{
wenzelm@41511
    13
  echo
wenzelm@41511
    14
  echo "Usage: isabelle $PRG [OPTIONS]"
wenzelm@41511
    15
  echo
wenzelm@41511
    16
  echo "  Options are:"
wenzelm@41511
    17
  echo "    -i           short identification (derived from Mercurial id)"
wenzelm@41511
    18
  echo
wenzelm@41511
    19
  echo "  Display Isabelle version information."
wenzelm@41511
    20
  echo
wenzelm@41511
    21
  exit 1
wenzelm@41511
    22
}
wenzelm@41511
    23
wenzelm@41511
    24
function fail()
wenzelm@41511
    25
{
wenzelm@41511
    26
  echo "$1" >&2
wenzelm@41511
    27
  exit 2
wenzelm@41511
    28
}
wenzelm@41511
    29
wenzelm@41511
    30
wenzelm@41511
    31
## process command line
wenzelm@41511
    32
wenzelm@41511
    33
# options
wenzelm@41511
    34
wenzelm@41511
    35
SHORT_ID=""
wenzelm@41511
    36
wenzelm@41511
    37
while getopts "i" OPT
wenzelm@41511
    38
do
wenzelm@41511
    39
  case "$OPT" in
wenzelm@41511
    40
    i)
wenzelm@41511
    41
      SHORT_ID=true
wenzelm@41511
    42
      ;;
wenzelm@41511
    43
    \?)
wenzelm@41511
    44
      usage
wenzelm@41511
    45
      ;;
wenzelm@41511
    46
  esac
wenzelm@41511
    47
done
wenzelm@41511
    48
wenzelm@41511
    49
shift $(($OPTIND - 1))
wenzelm@41511
    50
wenzelm@41511
    51
wenzelm@41511
    52
# args
wenzelm@41511
    53
wenzelm@41511
    54
[ "$#" -ne 0 ] && usage
wenzelm@41511
    55
wenzelm@41511
    56
wenzelm@41511
    57
## main
wenzelm@41511
    58
wenzelm@41511
    59
if [ -n "$SHORT_ID" ]; then
wenzelm@41511
    60
  if [ -n "$ISABELLE_ID" ]; then
wenzelm@41511
    61
    echo "$ISABELLE_ID"
wenzelm@41511
    62
  else
wenzelm@48837
    63
    "${HG:-hg}" id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined
wenzelm@41511
    64
  fi
wenzelm@41511
    65
else
wenzelm@41511
    66
  echo 'unidentified repository version'    # filled in automatically!
wenzelm@41511
    67
fi