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.