Delete website_status-2019-09-23.md
InessaPawson opened this issue · 6 comments
I opened a PR for "webteam_meeting2019-09-23.md". It contains a more detailed account about the same meeting.
git rm <path-to-file> followed by commit. How are you doing your work?
@charris I don't have a permission.
You can make it part of the pull request. I can delete the file for you, but it is a bit of git fu worth learning. Which is why I was wondering what you were using to edit and generate PRs.
Thank you for explaining it! I usually use the online version of GitHub on macOS.
Ah, I'll take a look, the online version is pretty limited. If you end up doing a lot of PR type stuff it would be good to get set up with something better. I don't develop on the Mac, but there are a lot of folks who do. Should be documented somewhere -- or maybe that is something that needs improvement... In any case, with a better setup you could use your favorite (code) editor. I don't know what you would be most comfortable doing, which is what matters here.
When you refer to a PR it is usually a good idea to make a link, you can do that by adding #<PR number> in the text, in this case #2. It is also possible to use git to move/rename files rather than recreating them. Note that everything goes through git, I myself cannot delete the file without making a PR or pushing a commit directly to the branch. I also don't have permissions to edit your PR, you need to check a box to allow that when you make the PR.
I've deleted the file by using the web interface to make the commit by opening the file and hitting the trash can button. I was allowed to commit directly to the master branch, I suspect that you would need to make it a PR if you lack permissions. If you do a lot of work in this repository we should give you maintainer permissions.
@charris Chuck, thank you for taking care of that and, what’s more, for taking the time to write this comment! I’ve learned a lot from you in these past 6 months.