Skip to content

Commit

Permalink
chore: do not run workflow on push (#2718)
Browse files Browse the repository at this point in the history
In this PR:
- Remove `on.push` trigger so that the workflow doesn't run against a
specific branch.

Official doc:
https://docs.github.com/en/actions/using-workflows/workflow-syntax-for-github-actions#onpushbranchestagsbranches-ignoretags-ignore
  • Loading branch information
JoeWang1127 authored and lqiu96 committed May 22, 2024
1 parent c3c4782 commit 83f8741
Showing 1 changed file with 5 additions and 8 deletions.
13 changes: 5 additions & 8 deletions .github/workflows/verify_library_generation.yaml
Original file line number Diff line number Diff line change
@@ -1,11 +1,6 @@
on:
push:
branches:
- main
pull_request:
# do not run this workflow when merging the pull request.
types: [opened, reopened, edited, synchronize]
workflow_dispatch:

name: verify_library_generation
jobs:
should-run-library-generation-tests:
Expand All @@ -21,9 +16,11 @@ jobs:
shell: bash
run: |
set -ex
git checkout "${base_ref}" # Checkout a detached head, and then fetch the base ref to populate the detached head.
# Checkout a detached head, and then fetch the base ref to populate the detached head.
git checkout "${base_ref}"
git fetch --no-tags --prune origin +${base_ref}:refs/remotes/origin/${base_ref}
git checkout "${head_ref}" # Checkout a detached head, and then fetch the head ref to populate the detached head.
# Checkout a detached head, and then fetch the head ref to populate the detached head.
git checkout "${head_ref}"
git fetch --no-tags --prune origin +${head_ref}:refs/remotes/origin/${head_ref}
changed_directories="$(git diff --name-only ${base_ref} ${head_ref})"
if [[ ${changed_directories} =~ "library_generation/" ]]; then
Expand Down

0 comments on commit 83f8741

Please sign in to comment.