author | wenzelm |
Thu, 17 Jul 2008 21:23:08 +0200 | |
changeset 27647 | ee452b218407 |
parent 27646 | d010fc1d3c46 |
child 27648 | 70973f73f09d |
Admin/makedist | file | annotate | diff | comparison | revisions |
--- 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