-
Notifications
You must be signed in to change notification settings - Fork 257
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Moving release procedures into a dev folder instead of the user-facing docs folder #2840
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is there a reason to rename from docs/dev/RELEASE
to dev/RELEASE
?
The docs folder contains user-facing documentation (which is copied as is into the documentation snapshots). The Release procedure is development information. Robin wanted it kept in git (I had earlier proposed moving it to the wiki). So a dev folder seemed a good solution. Other ideas are welcome. |
We could exclude it from the build if we really want to not have it on the public website, but But is it really bad to have it on the website? Having a "developer documentation" section is a good thing, I would think. |
Abandoning this PR -- not moving the dev material - instead not copying it into the snapshots -- cf. PR 2845 |
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.