equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # Author: Stefan Berghofer, TU Muenchen |
3 # Author: Stefan Berghofer, TU Muenchen |
|
4 # Author: Makarius |
4 # |
5 # |
5 # DESCRIPTION: display Isabelle version |
6 # DESCRIPTION: display Isabelle version |
6 |
7 |
7 echo 'unidentified repository version' # filled in automatically! |
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 |
|
63 ${HG:-hg} id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined |
|
64 fi |
|
65 else |
|
66 echo 'unidentified repository version' # filled in automatically! |
|
67 fi |