diff options
Diffstat (limited to '.github/workflows/build.yml')
-rw-r--r-- | .github/workflows/build.yml | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 50d1561..6e6a6d2 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -1,26 +1,19 @@ name: Tests +# bpo-40548: "paths-ignore" is not used to skip documentation-only PRs, because +# it prevents to mark a job as mandatory. A PR cannot be merged if a job is +# mandatory but not scheduled because of "paths-ignore". on: push: branches: - master - 3.8 - 3.7 - paths-ignore: - - 'Doc/**' - - 'Misc/**' - - '**/*.md' - - '**/*.rst' pull_request: branches: - master - 3.8 - 3.7 - paths-ignore: - - 'Doc/**' - - 'Misc/**' - - '**/*.md' - - '**/*.rst' jobs: build_win32: |