Run "tools" job on PR when commit message starts with "Update RLS/miri/..."

This commit is contained in:
kennytm 2018-07-03 06:01:58 +08:00
parent 20231d774b
commit 689cffa211
No known key found for this signature in database
GPG Key ID: FEF6C8051D0E013C

View File

@ -169,7 +169,7 @@ matrix:
- env: IMAGE=x86_64-gnu-aux
if: branch = auto
- env: IMAGE=x86_64-gnu-tools
if: branch = auto
if: branch = auto OR (type = pull_request AND commit_message =~ /(?i:^update.*\b(rls|rustfmt|clippy|miri)\b)/)
- env: IMAGE=x86_64-gnu-debug
if: branch = auto
- env: IMAGE=x86_64-gnu-nopt