changeset 40573 | 113ccf02d323 |
parent 37485 | 64b0356d0f19 |
child 40713 | 7f745e4b7cce |
--- 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"