How to add/move/remove sources¶
git grep for a source file “close to” the one you want to introduce. Then you will see where it is to be listed.
How to move/remove sources¶
git grep for the source file name. Then you will see where it is listed and you can move/remove it there.