# HG changeset patch
# User Chris Cannam
# Date 1452772986 0
# Node ID 6074fffd8a1d3fd2cc888a55bebf6e0e2a963997
# Parent  2c67e414ab463c98b226c8b3df736ba7b2e67f92
No, a bare repo is better

diff -r 2c67e414ab46 -r 6074fffd8a1d extra/soundsoftware/export-git.sh
--- a/extra/soundsoftware/export-git.sh	Thu Jan 14 10:54:56 2016 +0000
+++ b/extra/soundsoftware/export-git.sh	Thu Jan 14 12:03:06 2016 +0000
@@ -78,7 +78,6 @@
     authormap="$authordir/authormap_$reponame"
 
     git_repodir="$gitdir/$reponame"
-    git_workdir="$gitdir/$reponame.workdir"
 
     if [ ! -f "$authormap" ]; then
 	echo "No authormap file was created for repo $reponame, skipping"
@@ -96,14 +95,14 @@
     fi
     
     if [ ! -d "$git_repodir" ]; then
-	git init --separate-git-dir="$git_repodir" "$git_workdir"
+	git init --bare "$git_repodir"
     fi
 
     echo
     echo "About to run fast export for repo $reponame..."
     
     (
-	cd "$git_workdir"
+	cd "$git_repodir"
 
         # Force is necessary because git-fast-import (or git) can't handle
         # branches having more than one head ("Error: repository has at