author | wenzelm |
Wed, 17 Nov 2010 11:24:07 +0100 | |
changeset 40573 | 113ccf02d323 |
parent 40572 | 2315c3daee74 |
child 40574 | 226563829580 |
Admin/makedist | file | annotate | diff | comparison | revisions |
--- a/Admin/makedist Tue Nov 16 22:40:45 2010 +0100 +++ b/Admin/makedist Wed Nov 17 11:24:07 2010 +0100 @@ -108,7 +108,7 @@ if [ -z "$RELEASE" ]; then DISTNAME="Isabelle_$DATE" - DISTVERSION="Isabelle repository snapshot $IDENT ($DATE)" + DISTVERSION="Isabelle repository snapshot $IDENT $DATE" else DISTNAME="$RELEASE" DISTVERSION="$DISTNAME: $DISTDATE"