author | wenzelm |
Wed, 31 Mar 2021 18:12:46 +0200 | |
changeset 73520 | 4cba4e250c28 |
parent 73509 | 5d750df8e894 |
child 73521 | a6ca869af096 |
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)" |
|
73481 | 18 |
echo " -t symbolic tags (derived from Mercurial id)" |
41511 | 19 |
echo |
20 |
echo " Display Isabelle version information." |
|
21 |
echo |
|
22 |
exit 1 |
|
23 |
} |
|
24 |
||
25 |
function fail() |
|
26 |
{ |
|
27 |
echo "$1" >&2 |
|
28 |
exit 2 |
|
29 |
} |
|
30 |
||
31 |
||
32 |
## process command line |
|
33 |
||
34 |
# options |
|
35 |
||
36 |
SHORT_ID="" |
|
73481 | 37 |
TAGS="" |
41511 | 38 |
|
73481 | 39 |
while getopts "it" OPT |
41511 | 40 |
do |
41 |
case "$OPT" in |
|
42 |
i) |
|
43 |
SHORT_ID=true |
|
44 |
;; |
|
73481 | 45 |
t) |
46 |
TAGS=true |
|
47 |
;; |
|
41511 | 48 |
\?) |
49 |
usage |
|
50 |
;; |
|
51 |
esac |
|
52 |
done |
|
53 |
||
54 |
shift $(($OPTIND - 1)) |
|
55 |
||
56 |
||
57 |
# args |
|
58 |
||
59 |
[ "$#" -ne 0 ] && usage |
|
60 |
||
61 |
||
62 |
## main |
|
63 |
||
73481 | 64 |
if [ -z "$SHORT_ID" -a -z "$TAGS" ]; then |
67866 | 65 |
echo 'repository version' # filled in automatically! |
41511 | 66 |
fi |
73481 | 67 |
|
73482 | 68 |
HG_ARCHIVAL="$ISABELLE_HOME/.hg_archival.txt" |
69 |
||
73483 | 70 |
export LANG=C |
71 |
export HGPLAIN= |
|
72 |
||
73481 | 73 |
if [ -n "$SHORT_ID" ]; then |
73520
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73509
diff
changeset
|
74 |
if [ -f "$ISABELLE_HOME/etc/ISABELLE_ID" ]; then |
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73509
diff
changeset
|
75 |
ID="$(cat "$ISABELLE_HOME/etc/ISABELLE_ID")" |
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73509
diff
changeset
|
76 |
echo "$ID" |
73482 | 77 |
elif [ -f "$HG_ARCHIVAL" ]; then |
73509 | 78 |
RESULT="$(grep "^node:" < "$HG_ARCHIVAL" | cut -d " " -f2 | head -c12)" |
73481 | 79 |
[ -n "$RESULT" ] && echo "$RESULT" |
73520
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73509
diff
changeset
|
80 |
elif [ -d "$ISABELLE_HOME/.hg" ]; then |
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73509
diff
changeset
|
81 |
"${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || exit "$?" |
73481 | 82 |
fi |
83 |
fi |
|
84 |
||
85 |
if [ -n "$TAGS" ]; then |
|
86 |
RESULT="" |
|
87 |
if [ -d "$ISABELLE_HOME/.hg" ]; then |
|
88 |
RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" id -t 2>/dev/null) |
|
89 |
RC="$?" |
|
73482 | 90 |
elif [ -f "$HG_ARCHIVAL" ]; then |
73509 | 91 |
RESULT="$(grep "^tag:" < "$HG_ARCHIVAL" | cut -d " " -f2)" |
73481 | 92 |
RC="$?" |
93 |
fi |
|
94 |
if [ "$RC" -ne 0 ]; then |
|
95 |
exit "$RC" |
|
96 |
elif [ -n "$RESULT" -a "$RESULT" != "tip" ]; then |
|
97 |
echo "$RESULT" |
|
98 |
fi |
|
99 |
fi |