author | wenzelm |
Wed, 29 Aug 2018 20:01:39 +0200 | |
changeset 68847 | 511d163ab623 |
parent 67872 | 39b27d38a54c |
child 73480 | 0e880b793db1 |
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 |
|
67872
39b27d38a54c
more accurate isabelle_id: parent directory is not necessarily at tip;
wenzelm
parents:
67866
diff
changeset
|
63 |
"${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || echo undefined |
41511 | 64 |
fi |
65 |
else |
|
67866 | 66 |
echo 'repository version' # filled in automatically! |
41511 | 67 |
fi |