Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Error out if a PR is sent to the wrong channel #84997

Merged
merged 3 commits into from
May 15, 2021
Merged

Error out if a PR is sent to the wrong channel #84997

merged 3 commits into from
May 15, 2021

Commits on May 6, 2021

  1. move the current channel to src/ci/channel 

    This will make it easier for tools to programmatically detect which
channel CI is building.
    @pietroalbini
    pietroalbini committed May 6, 2021
    Configuration menu
    Copy the full SHA
    81a97ce View commit details
    Browse the repository at this point in the history

  2. ci: error out if someone sends a PR to the wrong branch

    @pietroalbini
    pietroalbini committed May 6, 2021
    Configuration menu
    Copy the full SHA
    392723e View commit details
    Browse the repository at this point in the history

Commits on May 12, 2021

  1. make verify-channel.sh compatible with macOS

    @pietroalbini
    pietroalbini committed May 12, 2021
    Configuration menu
    Copy the full SHA
    a8da333 View commit details
    Browse the repository at this point in the history