Git user identity should be set in the repo we're actually pushing.

tmiw · Mar 16, 2024 · 2c86d49 · 2c86d49
1 parent 71c4d36
commit 2c86d49
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/.github/workflows/render_user_manual.yml b/.github/workflows/render_user_manual.yml
@@ -31,15 +31,15 @@ jobs:
     - name: Push to github.io
       shell: bash
       run: |
-          git config --local user.email "$(git log --format='%ae' HEAD^!)"
-          git config --local user.name "$(git log --format='%an' HEAD^!)"
           export git_hash=$(git describe --always HEAD)
           git clone -b gh-pages `git remote get-url origin` website
           cd website
           git rm -rf * && rm -rf *
           cd ..
           mv manual/build/* website
           cd website
+          git config --local user.email "$(git log --format='%ae' HEAD^!)"
+          git config --local user.name "$(git log --format='%an' HEAD^!)"
           git add *
           git commit -am "Generated user manual from Git commit ${git_hash}"
           git push