--- a/Admin/lib/Tools/makedist Sat Oct 15 11:38:03 2016 +0200
+++ b/Admin/lib/Tools/makedist Sat Oct 15 13:07:54 2016 +0200
@@ -118,6 +118,8 @@
DIR="$DISTBASE/$DISTNAME"
[ -e "$DIR" ] && fail "Directory \"$DIR\" already exists"
+rm -f "$DISTPREFIX/ISABELLE_DIST" "$DISTPREFIX/ISABELLE_IDENT"
+
# retrieve repository archive
@@ -212,8 +214,8 @@
cd "$DISTBASE"
-echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
-echo "$IDENT" >../ISABELLE_IDENT
+echo "$DISTBASE/$DISTNAME.tar.gz" > "$DISTPREFIX/ISABELLE_DIST"
+echo "$IDENT" > "$DISTPREFIX/ISABELLE_IDENT"
chown -R "$LOGNAME" "$DISTNAME"
chmod -R g=o "$DISTNAME"