Now that we have added github login to gl.mathhub.info (see #190), we should think about what we want to do with it. For instance,
we definitely want to say something about this new feature on the entry page
we may want to get rid of duplicate accounts (e.g. I have two: mkohlhase (locally) and one via github).
what about synchronizing with MathHub.info proper? Do we have github accounts there as well?
we may need to rethink our use of "internal" repositories, they are now visible to the world: everyone with a github account can log in and see them in principle.
I am sure there is more
We should discuss this and find a joint intution cc: @tkw1536 @m-iancu @cmaeder @aoripov @jbs1
Now that we have added github login to gl.mathhub.info (see #190), we should think about what we want to do with it. For instance,