changeset 67865 | ab0b8e388967 |
parent 48837 | d1d806a42c91 |
child 67866 | 11e4060bcdca |
--- a/lib/Tools/version Thu Mar 15 11:27:32 2018 +0100 +++ b/lib/Tools/version Thu Mar 15 11:44:07 2018 +0100 @@ -60,7 +60,7 @@ if [ -n "$ISABELLE_ID" ]; then echo "$ISABELLE_ID" else - "${HG:-hg}" id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined + "${HG:-hg}" -R "$ISABELLE_HOME" id -i -r tip 2>/dev/null || echo undefined fi else echo 'unidentified repository version' # filled in automatically!