My first instinct was to create an issue on Github. But while trying to do so I was met with this message:
If you have a question please search or post to our Discourse site: https://discourse.julialang.org.
We use the GitHub issue tracker for bug reports and feature requests only.
Now I am not sure if this is considered a bug, because technically it is not breaking anything. Also it might not be a feature since no behaviour would change.
If possible I would still like to fix this, but I do not know what the correct process to follow would be. Can someone please describe the steps I need to take to fix this? Or alternatively tell me that this is nitpicking and not worth any action.
Cool, that you directly want to contribute – and welcome to discourse
If you are not sure you could open an issue with Pkg.jl here Issues · JuliaLang/Pkg.jl · GitHub
If you directly know how to fix that (for example which export to delete) you will have to fort that repository. probably clone that locally to your machine, read about development mode (if you want to be sure all tests still run fine), fix that locally, commit, push, and do a PR directly here https://github.com/JuliaLang/Pkg.jl/pulls
I am not 100% sure how much of the Git/GitHub workflow (fork-branch-fix-pullrequeest) you know, so maybe the explanation above is either too short or trivial to you
Overall I think it is not a bug, but nicer and cleaner code is always nice, I think, so feel free to contribute
I am working on making a pull request. I have read about the Git/Github forking workflow, but never used it myself. So I am using this to learn that workflow as @lrnv pointed out.
If I were to do this, I would fork (via the fork button in the top right of the github page for the repository), make the change in the forked repo via github.com, and after the cange, press the pop-up saying something like “this branch is ahead of …” to make the pull request.
Not sure if that is the best way, but it is very easy and fast, and has worked fine for me in making small changes to e.g. documentation, which I know do not break anything.
For small changes like this, the easiest thing is generally to use the edit button on github, which lets you make the change directly in your browser, and automates the process of creating the fork and the pull request.