Skip to content

Conversation

milessabin
Copy link
Contributor

No description provided.

@milessabin milessabin requested a review from smarter April 20, 2021 08:43
@milessabin milessabin self-assigned this Apr 20, 2021
@smarter smarter enabled auto-merge April 20, 2021 08:50
@smarter
Copy link
Member

smarter commented Apr 20, 2021

into master from topic/update-shapeless

Looks like you created a branch in the main dotty repo itself instead of in your fork, it works but it means the CI runs twice, so best to avoid that.

@smarter smarter disabled auto-merge April 20, 2021 10:24
@smarter smarter merged commit 3bcdc34 into master Apr 20, 2021
@smarter smarter deleted the topic/update-shapeless branch April 20, 2021 10:24
@milessabin
Copy link
Contributor Author

Looks like you created a branch in the main dotty repo itself instead of in your fork, it works but it means the CI runs twice, so best to avoid that.

Whoops! Sorry about that :-(

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.

2 participants