Join GitHub today
GitHub is home to over 40 million developers working together to host and review code, manage projects, and build software together.Sign up
Chore: update release script for new website repo #12006
What is the purpose of this pull request? (put an "X" next to item)
[ ] Documentation update
What changes did you make? (Give an overview)
This updates the release script now that we've change the website repository name to
Is there anything you'd like reviewers to focus on?
I've already changed the repository name, turned off publishing to GitHub Pages, and have updated the Jenkins script. Did I miss anything?
That’s an interesting point. Do you mean to rename the repository or just the name of the directory when we clone it in the release script? My inclination is that it’s probably fine as is since the releases are mostly run in Jenkins, but I don’t have a strong opinion and am happy to change it if others are concerned!