Commit 79dd6edd authored by Robert Bradshaw's avatar Robert Bradshaw

Fix make repo.

parent 739e97dc
...@@ -9,9 +9,12 @@ local: ...@@ -9,9 +9,12 @@ local:
.git: REV := $(shell cat .gitrev) .git: REV := $(shell cat .gitrev)
.git: TMPDIR := $(shell mktemp -d tmprepo.XXXXXX) .git: TMPDIR := $(shell mktemp -d tmprepo.XXXXXX)
.git: .git:
rm -rf $(TMPDIR)
git clone $(REPO) $(TMPDIR) git clone $(REPO) $(TMPDIR)
cd $(TMPDIR); git checkout -b working $(REV) 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 mv $(TMPDIR)/Doc/s5 Doc/s5
rm -rf $(TMPDIR) rm -rf $(TMPDIR)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment