From: Ulya Trofimovich <skvadrik@gmail.com>
Date: Sun, 9 Apr 2017 19:58:32 +0000 (+0100)
Subject: Use `git archive` insted of `git worktree` to sync with master.
X-Git-Url: https://granicus.if.org/sourcecode?a=commitdiff_plain;h=809cc00bc30e2bd25275bce5575ee0a205e0de81;p=re2c

Use `git archive` insted of `git worktree` to sync with master.
---

diff --git a/mk.sh b/mk.sh
index d0567e26..c969c0f0 100755
--- a/mk.sh
+++ b/mk.sh
@@ -1,11 +1,10 @@
 #!/bin/sh
 
-[ -d master ] || { 
-    git worktree prune
-    git worktree add master master
-}
-[ -e src/manual/options/options.rst_  ] ||  #merge manual tree from master
-     (cd master/re2c/doc/; tar cf - manual/) | (cd src/; tar xfp -) 
+# sync with master (pull manpage files)
+remote=`git config branch.master.remote` \
+    && git fetch $remote \
+    && git archive --remote=. remotes/$remote/master re2c/doc/manual \
+    | tar -C src/ --strip-components=2 -xpf -
 
 sphinx-build -b html src obj