Merge pull request #838 from chrisribe/PublishDocsToWiki

Publish docs to wiki

.github/workflows/publish_docs_to_wiki.yml

@@ -0,0 +1,39 @@
+name: Publish docs to Wiki
+
+# Trigger this action only if there are changes pushed to the doc/** directory under the main branch
+on:
+  push:
+    paths:
+      - doc/** # This includes all sub folders
+    branches:
+      - PublishDocsToWiki # This can be changed to any branch of your preference
+
+env:
+  USER_TOKEN: ${{ secrets.GH_WIKI_PAT }} # This is the repository secret personal access token
+  USER_NAME: ${{ vars.BOT_USER_NAME }} # Enter the username of your (bot) account
+  OWNER: ${{ github.event.repository.owner.name }} # This is the repository owner
+  REPOSITORY_NAME: ${{ github.event.repository.name }} # This is the repository name
+
+jobs:
+  publish_docs_to_wiki:
+    name: Publish docs to Wiki
+    runs-on: ubuntu-latest
+    steps:  
+      - name: Checkout repository
+        uses: actions/checkout@v3
+
+      # 1. Clone the current wiki master branch to a folder named `tmp_wiki`
+      - name: Pull content from wiki
+        run: |
+          git config --global user.name "$USER_NAME"
+          git config --global user.email "$USER_NAME"@users.noreply.github.com
+          git clone https://"$USER_TOKEN"@github.com/"$OWNER"/"$REPOSITORY_NAME".wiki.git tmp_wiki
+      # 4. Synchronize differences between `doc` & `tmp_wiki`
+      # 5. Push new Wiki content
+      - name: Push main repo content to wiki
+        run: |
+          rsync -av --delete doc/ tmp_wiki/ --exclude .git
+          cd tmp_wiki
+          git add .
+          git commit -m "Updated Wiki content" 
+          git push origin master