git - how to delete files in the remote repository?

Question

I am not sure what is the exact term for this problem. Basically, I need to remove some files & directory on my remote repository

I have a local git repo & remote repo in github

1. Had been working myself.
2. A friend made a pull request.
3. I merged his request (via github interface)
4. I pulled the changes.
5. I tested the code and decided not to take his changes (shouldn't have merged at the first place)
6. I reverted back to a previous commit
7. Made some changes
8. Push to the server.

This is how my local repository looks like at the moment:

*   7e143b1  (HEAD)
|  
| *   18cea0f  (origin/master, origin/HEAD, master)
| |  
| | * fc19ccf 
* | | 6f3c58a 
|/ /  
* | 8d82486 
|/  
| * d3ce65f  (pre-install-activeadmin)
|/  
* 7d0566c 
* d1c77ab 
* 75ba704 
* 30dc67c  (heroku/master)
* f89b1f6 
* ea5e2db 
* 08931d6 
* 9773a6f 
* b636aba 
* cb6f8d4 

I can change my local repo to 7d0566c. I am not sure where the head on my remote repo is pointing to.

How do I remove those files that are on remote repo but are not on my local repo?

Obviously, I do not see any of his files in my local repo because I did a reset of my HEAD to a previous commit. However, the remote repo still shows his files. When I commit, it commits just fine.

Is my workflow wrong? I should have just tested the patch at the first place. Any suggestion? I am new to version control. Thank you

Answer 1

Pull the changes from the server, then do a git rm on your local repo, commit the changes, and push to the server. The files will be deleted.