Update for pull request builds on GitHub

Hey all,

We currently use Azure Pipelines for CI builds on all pull requests that are filed on GitHub. Up till now, these builds have automatically been run whenever a PR was submitted or updated.

Starting today, we’re turning these automatic runs off in favor of comment-based triggers to experiment with finer-grained control over these builds. Folks may notice these comment triggers showing up on PRs and builds being delayed until those comments are posted.

Submitters do not need to do anything differently. Only repository maintainers can trigger builds, and we have processes in place to submit these triggers on a regular basis.

Please let us know if you have any questions. Thanks!

  • Sunya