# HG changeset patch
# User wenzelm
# Date 1476350532 -7200
# Node ID c69a77e0124a770bdd8a9099602e1014dd207e47
# Parent  857a335ac292ecda67c0444bebaeb22d0c089a7e
more cleanup;

diff -r 857a335ac292 -r c69a77e0124a Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist	Thu Oct 13 09:52:54 2016 +0200
+++ b/Admin/lib/Tools/makedist	Thu Oct 13 11:22:12 2016 +0200
@@ -199,6 +199,9 @@
 
 ./bin/isabelle java isabelle.NEWS
 
+rmdir "$USER_HOME/.isabelle/${DISTNAME}-build"
+rmdir "$USER_HOME/.isabelle/${DISTNAME}"
+
 
 # create archive