Fix make repo.

diff --git a/Makefile b/Makefile
index 964204fd47d47a54965e7b7c37d1cc9b463565f4..7a95311b3052258fc06f55b18e95a072f26e09d2 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -9,9 +9,12 @@ local:
 .git: REV := $(shell cat .gitrev)
 .git: TMPDIR := $(shell mktemp -d tmprepo.XXXXXX)
 .git: 
+       rm -rf $(TMPDIR)
        git clone $(REPO) $(TMPDIR)
        cd $(TMPDIR); git checkout -b working $(REV)
-       mv $(TMPDIR)/{.git,.hgtags,.hgignore} .
+       mv $(TMPDIR)/.hgtags .
+       mv $(TMPDIR)/.hgignore .
+       mv $(TMPDIR)/.git .
        mv $(TMPDIR)/Doc/s5 Doc/s5
        rm -rf $(TMPDIR)