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

Update to new coverage tools release #10393

Closed
wants to merge 1 commit into from

Conversation

ulfjack
Copy link
Contributor

@ulfjack ulfjack commented Dec 9, 2019

Change-Id: I2cb5f90c75e341419bb05d035b0ae1cc26a5eba5

Change-Id: I2cb5f90c75e341419bb05d035b0ae1cc26a5eba5
@bazel-io bazel-io closed this in 9588a9e Dec 10, 2019
@ulfjack ulfjack deleted the coverage branch January 22, 2020 10:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants