diff -r d65835c381dd -r 6aa69999da8f Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Mon Mar 14 12:34:12 2011 +0100 +++ b/Admin/isatest/isatest-makedist Mon Mar 14 15:13:00 2011 +0100 @@ -83,6 +83,7 @@ ISABELLE_DIST=`cat $DISTPREFIX/ISABELLE_DIST` $TAR xvzf $ISABELLE_DIST >> $DISTLOG 2>&1 ln -sf $(basename $ISABELLE_DIST .tar.gz) Isabelle +cp Isabelle/etc/settings Isabelle/etc/settings.orig ssh atbroy102 "rm -rf /home/isatest/isadist && mkdir -p /home/isatest/isadist" && \ rsync -a "$HOME/isadist/." atbroy102:/home/isatest/isadist/.