Merge remote-tracking branch 'origin/master' into mypy

Author: basnijholt

azure-pipelines.yml

@@ -7,6 +7,8 @@ pr:
 
 jobs:
 - job: authors_check
+  pool:
+    vmImage: 'ubuntu-latest'
   steps:
   - script: |
       MISSING_AUTHORS=$(git shortlog -s HEAD | sed -e "s/^[0-9\t ]*//"| xargs -i sh -c 'grep -q "{}" AUTHORS.md || echo "{} missing from authors"')