diff -r ab0b8e388967 -r 11e4060bcdca lib/Tools/version
--- 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