| changeset 67866 | 11e4060bcdca |
| parent 67865 | ab0b8e388967 |
| child 67872 | 39b27d38a54c |
| 67865:ab0b8e388967 | 67866:11e4060bcdca |
|---|---|
61 echo "$ISABELLE_ID" |
61 echo "$ISABELLE_ID" |
62 else |
62 else |
63 "${HG:-hg}" -R "$ISABELLE_HOME" id -i -r tip 2>/dev/null || echo undefined |
63 "${HG:-hg}" -R "$ISABELLE_HOME" id -i -r tip 2>/dev/null || echo undefined |
64 fi |
64 fi |
65 else |
65 else |
66 echo 'unidentified repository version' # filled in automatically! |
66 echo 'repository version' # filled in automatically! |
67 fi |
67 fi |