Documenter.jl: zeptodoctor appears as contributor when using Documenter.jl

Created on 29 Jul 2020  路  11Comments  路  Source: JuliaDocs/Documenter.jl

Hi, it is not super crucial but quite a bit annoying/surprising when using Documenter.jl

because of these two lines:

run(`git config user.name "zeptodoctor"`)
run(`git config user.email "[email protected]"`)

Using documenter actually brings in zeptodoctor as a contributor to whatever github repository uses Documenter.jl
that is quite drastical, as there is no way to get a contributor out of a repository again, even if it is artificial like this.

Best would be to just don't have this, but if this is really necessary, please add a big warning into the Documentation of Documenter.jl where people can see it and decide whether they want this or not.

Most helpful comment

Should we maybe just retire @zeptodoctor? Have we actually gotten anything from having that account?

All 11 comments

I have noticed it popping up as well.

as there is no way to get a contributor out of a repository again

Actually, zepotdoctor only commits to gh-pages, so simply squashing that branch (no real loss there) and force pushing should get rid of it (together with a change in Documenter).

GitHub used to only count contributions to the master branch but apparently that is not true anymore.

Should we maybe just retire @zeptodoctor? Have we actually gotten anything from having that account?

@fredrikekre Not really. Counting contributions on gh-pages is as old as contributions themselves. See Introducing contributions from GitHub blog.

Regarding this issue, zeptodoctor surely doesn't have to be authenticated as an user. For example, I think Travis-related commits are logged as dummy user, not associated with any GitHub account. Although GitHub Actions-related commits are logged as such. Why do they do that? I have no clue.

@fredrikekre Not really. Counting contributions on gh-pages is as old as contributions themselves. See Introducing contributions from GitHub blog.

That is on a user profile. I am talking about repo contributions. Actually, GitHub docs still say:

If all your commits in the repository are on non-default branches, you won't be in the contributors graph. For example, commits on the gh-pages branch aren't included in the graph unless gh-pages is the repository's default branch


Regarding this issue, zeptodoctor surely doesn't have to be authenticated as an user.

It is not. You can put in any email and name and pretend you are someone.

It is not. You can put in any email and name and pretend you are someone.

What do you mean by this exactly? Do you agree with my statement or not? There's a security barrier nevertheless, since you need push access to the repository (or deploy keys and secrets).

I mean that I can pretend to be you: https://github.com/JuliaDocs/Documenter.jl/commit/7863089208445888deab2237c278685f9946f6f8 the same way documenter pretends to be @zeptodoctor. @zeptodoctor does not have access to any repos.

If I remember correctly, the reason we set @zeptodoctor up was that we could see some representation of Documenter use on its contributions graph. That actually doesn't work, since only JuliaDocs and JuliaLang orgs show up there.

So, how about we:

  • [x] Delete the @zeptodoctor user account
  • [x] Update the email address in Documenter to something like [email protected]

@fredrikekre, I think only you have access to @zeptodoctor if I recall correctly?

BTW, it does not show up in the repo contributions page: https://github.com/JuliaDocs/Documenter.jl/graphs/contributors so I think this is a bug in GitHub's new repo-overview page.

The repo contributions page is actually correct. They state explicitly, that they only count contributions to master.
Screenshot 2020-08-05 at 21 11 17

When I opened a ticket to github about the surprising zeptodoctor contributor, I also referred to the contributors page, but they just said that contributor shows master only, while as zeptodoctor commited to gh-pages branch, it appears on the front page as a contributor. Apparently it is intended behaviour now.

We deleted @zeptodoctor a few days and it has now finally disappeared from the contributors widgets.

Was this page helpful?
0 / 5 - 0 ratings

Related issues

jebej picture jebej  路  3Comments

cadojo picture cadojo  路  3Comments

denizyuret picture denizyuret  路  6Comments

lindnemi picture lindnemi  路  3Comments

haampie picture haampie  路  3Comments