From 809cc00bc30e2bd25275bce5575ee0a205e0de81 Mon Sep 17 00:00:00 2001
From: Ulya Trofimovich <skvadrik@gmail.com>
Date: Sun, 9 Apr 2017 20:58:32 +0100
Subject: [PATCH] Use `git archive` insted of `git worktree` to sync with
 master.

---
 mk.sh | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

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
 
-- 
2.40.0