Rename this repo to mybinder.org-user-guide

[consideRatio]

Scoping a git repository by a clear title is a big deal for its maintenance. I've not worked much in this repo and didn't know so well how to document things because of how this repository has been named. binder doesn't help me understand much besides its something related to binderhub, mybinder.org, or similar. But what exactly?

In #271 @choldgraf provided a new title, mybinder.org user documentation in the readme and it all became very clear to me, and I would love to have such clarity directly from the title instead.

Could we rename this repository to mybinder.org-user-documentation or mybinder.org-user-docs for example?

It seems that these documentation is published to RTD under mybinder.readthedocs.org, so there won't be broken URLs etc if we rename the repo as we can still publish to the same RTD URL.

[consideRatio]

• Current website title "Binder documentation"
• Current logo "Binder user guide"
• Current github repo "binder"
• Current website URL: mybinder.readthedocs.org

I suggest that we first seek agreement on what the scope of this repo is about.

Is there agreement that this is a "mybinder.org user guide" or "mybinder.org user documentation" ? 👍 to show agreement, 👀 to indicate your unsure, and comment to clarify what the scope of this repo currently is and if you think it should be adjusted to to something etc.

[choldgraf]

+1 from me - how about just binder-user-documentation ?

[consideRatio]

I overall dislike the use of binder as its unclear to me if its binderhub in general or mybinder.org focused documentation.

It seems binder is used to speak about a "Binder service" and "Binder repository". It seems focused on documenting the mybinder.org service rather than all binderhub services etc, but I'm unsure.

Overall I find that binder is a vague bucket term meaning many things, where it sometimes is used to mean a repo2docker/binderhub compatible repository, a binderhub deployment/service, or specifically the mybinder.org federation of binderhub services.

If this is named binder user documentation, I'm still not clear on what is meant or what makes sense to put in this repo.

[choldgraf]

The reason I used Binder instead of mybinder.org was because much of this documentation is generically useful for any BinderHub user, rather than just for mybinder.org. I didn't want to call in BinderHub User Documentation because I suspect most users don't (want to) think about the underlying hub implementation tool, they just "want to launch a binder repo".

Perhaps mybinder.org user documentation will OK, given that people understand the underlying service can be deployed elsewhere?

[betatim]

Given that the first sentence in the README is "This repository contains the documentation and usage instructions for the mybinder.org service." I'd go with mybinder.org-user-guide as repo name. At least then we are consistent :D

I agree that "binder" isn't a useful term when it comes to trying to be precise and unambiguous.

[manics]

I agree with mybinder.org-user-guide, or mybinder-user-guide since a . in a repo name always looks weird to me and people always call it "mybinder".

[consideRatio]

Since we have mybinder.org-deploy, i'm voting mybinder.org-user-guide, where we try to help non-mybinder.org users but stil focus on mybinder.org users and clarify if there is something mybinder.org specific perhaps?

[choldgraf]

+1 from me

I've updated the title so that it's clear what our current proposal is. IMO if there aren't any objections, we should implement this in a day or two.

Update: I think I remember why it's called binder/

The reason that this repository is vaguely named binder is because this repo is the source for the gitter.im/binder channel.

So we should double-check that renaming this repository won't rename that channel. If it does, then I suggest we find some other way to rename this repository's content without changing that channel name (e.g. we could create a new repository called mybinder.org-user-guide and then turn this repository into an empty one just for the gitter channel.

[betatim]

Another thing to check post rename: do links to the old name automatically redirect? If not that is something to fix as well

[consideRatio]

@betatim i think we are good as we use rtd hosting as compared to github pages hosting, so the github repo name isnt in the url.

[consideRatio]

I went ahead and did the name change and verified function of the gitter repository. There was a coupling with permissions to this repo, but I updated it to be a coupling to the jupyterhub gitter community admins, which in turn is coupled to the jupyterhub github organizations members. It was not possible to switch to mybinder.org-user-guide specific permissions but this should be fine.

@betatim @choldgraf can I be added as an admin for https://readthedocs.org/projects/mybinder/? I'd like to help migrate from master to main and make sure that the builds function still after the rename of this repo.

[consideRatio]

Super happy about this change!!! It makes me engage with this repo in an entirely new way since having a more clear scope makes me feel actionable of what can be done within it, and makes me understand it better etc. This is a very big deal for me as a contributor!

[choldgraf]

Added you as a maintainer!

This makes me think: we should track both GitHub handles and ReadTheDocs handles for all of our team members

[consideRatio]

Thank you @choldgraf!!

[consideRatio]

For reference, I learned now that there is also https://docs.mybinder.org that takes us to https://mybinder.readthedocs.org, which is enabled by a DNS entry and the mybinder.org specific redirector that is configured to redirect to mybinder.readthedocs.org, further strengthening the coupling to mybinder.org.

https://github.com/jupyterhub/mybinder.org-deploy/blob/f00c669edfa4c699faa024450c330b7309e0aad1/config/prod.yaml#L161-L164