equal
deleted
inserted
replaced
58 |
58 |
59 if [ -n "$SHORT_ID" ]; then |
59 if [ -n "$SHORT_ID" ]; then |
60 if [ -n "$ISABELLE_ID" ]; then |
60 if [ -n "$ISABELLE_ID" ]; then |
61 echo "$ISABELLE_ID" |
61 echo "$ISABELLE_ID" |
62 else |
62 else |
63 ${HG:-hg} id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined |
63 "${HG:-hg}" id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined |
64 fi |
64 fi |
65 else |
65 else |
66 echo 'unidentified repository version' # filled in automatically! |
66 echo 'unidentified repository version' # filled in automatically! |
67 fi |
67 fi |