equal
deleted
inserted
replaced
63 |
63 |
64 if [ -z "$SHORT_ID" -a -z "$TAGS" ]; then |
64 if [ -z "$SHORT_ID" -a -z "$TAGS" ]; then |
65 echo 'repository version' # filled in automatically! |
65 echo 'repository version' # filled in automatically! |
66 fi |
66 fi |
67 |
67 |
|
68 HG_ARCHIVAL="$ISABELLE_HOME/.hg_archival.txt" |
|
69 |
68 if [ -n "$SHORT_ID" ]; then |
70 if [ -n "$SHORT_ID" ]; then |
69 if [ -d "$ISABELLE_HOME/.hg" ]; then |
71 if [ -d "$ISABELLE_HOME/.hg" ]; then |
70 "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || exit "$?" |
72 "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || exit "$?" |
71 elif [ -f "$ISABELLE_HOME/.hg_archival.txt" ]; then |
73 elif [ -f "$HG_ARCHIVAL" ]; then |
72 RESULT="$(fgrep node: < "$ISABELLE_HOME/.hg_archival.txt" | cut -d " " -f2 | head -c12)" |
74 RESULT="$(fgrep node: < "$HG_ARCHIVAL" | cut -d " " -f2 | head -c12)" |
73 [ -n "$RESULT" ] && echo "$RESULT" |
75 [ -n "$RESULT" ] && echo "$RESULT" |
74 elif [ -n "$ISABELLE_ID" ]; then |
76 elif [ -n "$ISABELLE_ID" ]; then |
75 echo "$ISABELLE_ID" |
77 echo "$ISABELLE_ID" |
76 fi |
78 fi |
77 fi |
79 fi |
79 if [ -n "$TAGS" ]; then |
81 if [ -n "$TAGS" ]; then |
80 RESULT="" |
82 RESULT="" |
81 if [ -d "$ISABELLE_HOME/.hg" ]; then |
83 if [ -d "$ISABELLE_HOME/.hg" ]; then |
82 RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" id -t 2>/dev/null) |
84 RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" id -t 2>/dev/null) |
83 RC="$?" |
85 RC="$?" |
84 elif [ -f "$ISABELLE_HOME/.hg_archival.txt" ]; then |
86 elif [ -f "$HG_ARCHIVAL" ]; then |
85 RESULT="$(fgrep tag: < "$ISABELLE_HOME/.hg_archival.txt" | cut -d " " -f2)" |
87 RESULT="$(fgrep tag: < "$HG_ARCHIVAL" | cut -d " " -f2)" |
86 RC="$?" |
88 RC="$?" |
87 fi |
89 fi |
88 if [ "$RC" -ne 0 ]; then |
90 if [ "$RC" -ne 0 ]; then |
89 exit "$RC" |
91 exit "$RC" |
90 elif [ -n "$RESULT" -a "$RESULT" != "tip" ]; then |
92 elif [ -n "$RESULT" -a "$RESULT" != "tip" ]; then |