commit cac55f2eeaaedefe0316130c3bb1bad24b231694
parent da1406da5b51347a163cccfd3b6708f43a0f1b8f
Author: Amit Dutta <mail@amit.is-a.dev>
Date: Mon, 22 Jun 2026 20:12:55 +0530
Merge pull request #9 from notamitgamer/copilot/fix-docs-deployment-issues
Prevent bot-triggered deploy loops and persist generated docs to main
Diffstat:
2 files changed, 15 insertions(+), 6 deletions(-)
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -4,6 +4,8 @@ on:
push:
branches:
- main
+ paths-ignore:
+ - 'CHANGELOG.md'
workflow_dispatch:
permissions:
@@ -18,6 +20,7 @@ concurrency:
jobs:
sync-hf:
runs-on: ubuntu-latest
+ if: github.actor != 'github-actions[bot]'
steps:
- name: Checkout GitHub Repo
uses: actions/checkout@v4
@@ -55,6 +58,7 @@ jobs:
build:
runs-on: ubuntu-latest
+ if: github.actor != 'github-actions[bot]'
steps:
- name: Checkout
uses: actions/checkout@v4
@@ -81,13 +85,20 @@ jobs:
git log --pretty=format:"%H|%s|%an|%aI" -20 > git_log.txt
python changelog.py
- - name: Commit CHANGELOG.md to repo
+ - name: Commit generated docs and changelog to repo
run: |
git config user.name "github-actions[bot]"
git config user.email "github-actions[bot]@users.noreply.github.com"
+ if [ -d docs ]; then
+ git add docs
+ fi
git add CHANGELOG.md
- git commit -m "chore: update CHANGELOG.md [skip ci]" || echo "No changes"
- git push
+ if ! git diff --cached --quiet; then
+ git commit -m "chore: update generated docs and changelog [skip ci]"
+ git push
+ else
+ echo "No changes"
+ fi
- name: Setup Node.js
uses: actions/setup-node@v4
@@ -113,6 +124,7 @@ jobs:
name: github-pages
url: ${{ steps.deployment.outputs.page_url }}
runs-on: ubuntu-latest
+ if: github.actor != 'github-actions[bot]'
needs: build
steps:
- name: Deploy to GitHub Pages
diff --git a/.github/workflows/sync-to-hf.yml b/.github/workflows/sync-to-hf.yml
@@ -2,9 +2,6 @@ name: Manual and Auto Sync to Hugging Face
on:
workflow_dispatch:
- push:
- branches:
- - main
jobs:
sync-dataset:
