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