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

docs: remove dead link #12437

Closed
wants to merge 1 commit into from
Closed

docs: remove dead link #12437

wants to merge 1 commit into from

Conversation

connorjclark
Copy link
Collaborator

@connorjclark connorjclark requested a review from a team as a code owner May 3, 2021 21:44
@connorjclark connorjclark requested review from patrickhulce and removed request for a team May 3, 2021 21:44
@google-cla google-cla bot added the cla: yes label May 3, 2021
@connorjclark
Copy link
Collaborator Author

Or maybe we link to a specific commit?

@brendankenny
Copy link
Member

there was a start on this in #12390, not sure what happened...

@patrickhulce
Copy link
Collaborator

Ah that toolbox PR definitely seems to suggest it is dead though, I didn't realize the link I found was on master but they'd transitioned to main :) removal SGTM

@connorjclark
Copy link
Collaborator Author

connorjclark commented May 3, 2021

interesting to know it only took 12 days to not just get an issue, but a PR for a dead link! much faster than I would have guessed.

@patrickhulce
Copy link
Collaborator

How do we re-run the checks on a branch of a fork for the new requirements? Would be nice to give external credit :)

@patrickhulce
Copy link
Collaborator

fixed by #12390 :)

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

Successfully merging this pull request may close these issues.

4 participants