changeset 67872 | 39b27d38a54c |
parent 67866 | 11e4060bcdca |
child 73480 | 0e880b793db1 |
--- a/lib/Tools/version Thu Mar 15 22:17:56 2018 +0100 +++ b/lib/Tools/version Thu Mar 15 22:28:20 2018 +0100 @@ -60,7 +60,7 @@ if [ -n "$ISABELLE_ID" ]; then echo "$ISABELLE_ID" else - "${HG:-hg}" -R "$ISABELLE_HOME" id -i -r tip 2>/dev/null || echo undefined + "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || echo undefined fi else echo 'repository version' # filled in automatically!