changeset 27647 | ee452b218407 |
parent 27640 | 9df10b28aa60 |
child 28942 | 043a42ba2a4d |
--- a/Admin/makedist Thu Jul 17 21:22:44 2008 +0200 +++ b/Admin/makedist Thu Jul 17 21:23:08 2008 +0200 @@ -159,7 +159,7 @@ echo "IMPORTANT NOTE" echo "==============" echo - echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE." + echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE." echo } >ANNOUNCE else