-
Notifications
You must be signed in to change notification settings - Fork 1k
It translations #1828
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
It translations #1828
Conversation
@dwijnand where does this PR stand? |
|
ping @dwijnand |
@dwijnand is the CI failure real or spurious? |
No idea. Can't tell if it's a function of this PR not being merged or if it's flakiness or it could be something else. Either way, it's exhausted my patience. |
Oh, I've forced pushed here, but it's not my PR. |
"The repository that submitted this pull request has been deleted." @gabro perhaps you know someone who would be interested in reviving it? |
@SethTisue I'll ask around and post an update in case someone's interested! |
basics.md and tuples.md come from this pull request.