From c17afe47c4e1bc66ed8406a86246cd12a01c4665 Mon Sep 17 00:00:00 2001 From: Henry Date: Thu, 3 Sep 2020 12:26:06 +0200 Subject: [PATCH] Ignore .git directory (will be deleted otherwise) (#88) Co-authored-by: Henry Pauli --- .github/deploy_wiki.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/deploy_wiki.sh b/.github/deploy_wiki.sh index c0d0fe09..914236f1 100755 --- a/.github/deploy_wiki.sh +++ b/.github/deploy_wiki.sh @@ -56,7 +56,7 @@ tmp_dir=$(mktemp -d -t ci-XXXXXXXXXX) ) debug "Rsync contents of $WIKI_PATH" -rsync -q -a --delete "$GITHUB_WORKSPACE/$WIKI_PATH/" "$tmp_dir" +rsync -q -a --delete --exclude=.git "$GITHUB_WORKSPACE/$WIKI_PATH/" "$tmp_dir" if [ ! -r "$tmp_dir/Home.md" ]; then debug "Copy README.md to wiki/Home.md"