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.

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

Fix and Improve WASM CI #114

Merged
merged 2 commits into from
Oct 1, 2019
Merged

Fix and Improve WASM CI #114

merged 2 commits into from
Oct 1, 2019

Conversation

josephlr
Copy link
Member

Fixes #113

  • Always use latest Firefox
    • We have to use latest Chrome, so we might as well do the same thing here.
  • Explicitly pin wasmtime and cargo-web
    • We don't need a particular version here, so we might as well pin to avoid CI breakage.
  • Make sure our wasm-bindgen-test-runner and wasm-bindgen versions match
    • This uses the cargo metadata command (which is an awesome thing I just learned about).

We now consistently use the $VERSION environment variable to make our intentions explicit (and to avoid repeating version numbers).

- Use latest Firefox
- Explicitly pin wasmtime and cargo-web
- Make sure our `wasm-bindgen-test-runner` and `wasm-bindgen` versions match
@josephlr josephlr removed the request for review from dhardy October 1, 2019 07:26
@dhardy dhardy merged commit 7f013b1 into rust-random:master Oct 1, 2019
@josephlr
Copy link
Member Author

josephlr commented Oct 1, 2019

Hey @newpavlov @dhardy I still have Write access to this repo, but I wasn't able to merge this PR ("You’re not authorized to merge this pull request.") even though it was approved. Is this intentional, or did something change? I was able to merge #108 just fine a few days ago.

For the Google repos I maintain, I set the branch protection rules to be:

  • master is protected, so no force pushing
  • All PRs against master require approval
  • PRs require approval from at least one other user with Write permission
  • Once approved, anyone with Write access can merge the PR

I thought that's what getrandom had as well, but it seems like that's not the case.

@josephlr josephlr deleted the ci branch October 1, 2019 07:41
@dhardy
Copy link
Member

dhardy commented Oct 1, 2019

Sorry @josephlr, that was me; I demoted you from "Maintain" to Write access; according to the description this should still let you manage PRs so I don't know why this happened.

I checked the branch protection (merge review, push, and now status checks); these shouldn't be an issue. Hmm, I'll bump you back to Maintain then (according to the description the only difference is some repo settings).

@josephlr
Copy link
Member Author

josephlr commented Oct 1, 2019

Sorry @josephlr, that was me; I demoted you from "Maintain" to Write access; according to the description this should still let you manage PRs so I don't know why this happened.

That's really weird, I agree that the docs suggest I should only need Write permission to merge approved PRs. It might be a bug in Github's new permissions settings, or just some unclear docs. I haven't dealt that much with Triage/Maintain permissions as the new permissions Beta hasn't rolled out to the Google org yet.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

CI is broken for wasm-bindgen
3 participants