Closed consideRatio closed 1 year ago
Thank you for opening your first issue in this project! Engagement like this is essential for open source projects! :hugs:
If you haven't done so already, check out Jupyter's Code of Conduct. Also, please try to follow the issue template as it helps other other community members to contribute more effectively.
You can meet the other Jovyans by joining our Discourse forum. There is also an intro thread there where you can stop by and say Hi! :wave:
Welcome to the Jupyter community! :tada:
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" ? :+1: to show agreement, :eyes: 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.
+1 from me - how about just binder-user-documentation
?
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.
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?
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.
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".
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?
+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.
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.
Another thing to check post rename: do links to the old name automatically redirect? If not that is something to fix as well
@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.
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.
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!
Added you as a maintainer!
This makes me think: we should track both GitHub handles and ReadTheDocs handles for all of our team members
Thank you @choldgraf!!
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.
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 https://github.com/jupyterhub/binder/pull/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
ormybinder.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.