We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
If users make a typo or want to change the name to a better one, there is no option to do so currently.
Bart noted that the repo name is used as location on the server. A rename on the website should result in a move in the file system.
The text was updated successfully, but these errors were encountered:
Note that the name being used as a location is no longer true, so this is not a problem.
Sorry, something went wrong.
Solved by #4381.
No branches or pull requests
If users make a typo or want to change the name to a better one, there is no option to do so currently.
Bart noted that the repo name is used as location on the server. A rename on the website should result in a move in the file system.The text was updated successfully, but these errors were encountered: