diff options
author | Victor Stinner <vstinner@python.org> | 2020-05-07 20:42:14 (GMT) |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-07 20:42:14 (GMT) |
commit | 4e363761fc02a89d53aba4382dc451293bd6f0ba (patch) | |
tree | 55a61aafa747b7b5e8d6372c3f09d1554ae31869 | |
parent | c068b53a0ca6ebf740d98e422569d2f705e54f93 (diff) | |
download | cpython-4e363761fc02a89d53aba4382dc451293bd6f0ba.zip cpython-4e363761fc02a89d53aba4382dc451293bd6f0ba.tar.gz cpython-4e363761fc02a89d53aba4382dc451293bd6f0ba.tar.bz2 |
bpo-40548: Always run GitHub action, even on doc PRs (GH-19981)
Always run GitHub action jobs, even on documentation-only pull
requests. So it will be possible to make a GitHub action job, like
the Windows (64-bit) job, mandatory.
-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: |