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 dead link to grepcode #436

Merged
merged 1 commit into from
Dec 7, 2018
Merged

Update dead link to grepcode #436

merged 1 commit into from
Dec 7, 2018

Conversation

aki-ks
Copy link
Contributor

@aki-ks aki-ks commented Oct 14, 2018

Grepcode is dead. openjdk.java.net should be more lasting.

@aki-ks
Copy link
Contributor Author

aki-ks commented Oct 15, 2018

That's strange. I've just changed a comment. How can this cause the build to fail?

@Hydrotoast
Copy link
Contributor

Hi @aki-ks , I checked the build failure. I ran into the same issue in #438, which is a flaky test that occurs with a frequency of 1 / 1000 per build job (I believe there are ~10-15 build jobs per PR). The PR includes a fix in the second commit.

Due to the rarity of the flakiness, you can trigger a new build that should pass with a high probability of success. A build should be triggered when this PR detects a change in the source branch of the merge, which appears to be patch-1 of your repository.

I believe you can amend the the timestamp of the commit without changing the diff or the message and force push to your patch-1 branch. The following should work, but be sure that you are on the branch that has the desired change. :)

git commit --amend --no-edit
git push -f origin patch-1

@rickynils rickynils merged commit a10ce6d into typelevel:master Dec 7, 2018
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.

3 participants