changeset 67866 | 11e4060bcdca |
parent 67865 | ab0b8e388967 |
child 67872 | 39b27d38a54c |
--- a/lib/Tools/version Thu Mar 15 11:44:07 2018 +0100 +++ b/lib/Tools/version Thu Mar 15 11:49:29 2018 +0100 @@ -63,5 +63,5 @@ "${HG:-hg}" -R "$ISABELLE_HOME" id -i -r tip 2>/dev/null || echo undefined fi else - echo 'unidentified repository version' # filled in automatically! + echo 'repository version' # filled in automatically! fi