# HG changeset patch
# User Chris Cannam
# Date 1452767245 0
# Node ID 21098b932cb8f7e33852aaa2d9dc24e7c883743f
# Parent  a0c46d6fe7bceb9213f98d694a82c161eac01477
Separate out git repo dir and work dir (so as to serve repo dir only)

diff -r a0c46d6fe7bc -r 21098b932cb8 extra/soundsoftware/export-git.sh
--- a/extra/soundsoftware/export-git.sh	Thu Jan 14 09:56:38 2016 +0000
+++ b/extra/soundsoftware/export-git.sh	Thu Jan 14 10:27:25 2016 +0000
@@ -76,7 +76,9 @@
 
     reponame=$(basename "$hgrepo")
     authormap="$authordir/authormap_$reponame"
-    gitrepo="$gitdir/$reponame"
+
+    git_repodir="$gitdir/$reponame"
+    git_workdir="$gitdir/$reponame.workdir"
 
     if [ ! -f "$authormap" ]; then
 	echo "No authormap file was created for repo $reponame, skipping"
@@ -93,15 +95,15 @@
 	continue
     fi
     
-    if [ ! -d "$gitrepo" ]; then
-	git init "$gitrepo"
+    if [ ! -d "$git_repodir" ]; then
+	git init --separate-git-dir="$git_repodir" "$git_workdir"
     fi
 
     echo
     echo "About to run fast export for repo $reponame..."
     
     (
-	cd "$gitrepo"
+	cd "$git_workdir"
 
         # Force is necessary because git-fast-import (or git) can't handle
         # branches having more than one head ("Error: repository has at