author | wenzelm |
Fri, 06 Sep 2013 15:47:51 +0200 | |
changeset 53436 | ef2bb63583ac |
parent 53435 | 2220f0fb5581 |
child 53437 | b098d53152d9 |
child 53439 | 5bef05f5ed58 |
--- a/Admin/lib/Tools/makedist Fri Sep 06 12:46:50 2013 +0200 +++ b/Admin/lib/Tools/makedist Fri Sep 06 15:47:51 2013 +0200 @@ -140,7 +140,7 @@ echo "IMPORTANT NOTE" echo "==============" echo - echo "This is snapshot of Isabelle/${IDENT} from the repository." + echo "This is a snapshot of Isabelle/${IDENT} from the repository." echo } >ANNOUNCE else