Git stuff

Clone the main repository in a separate directory:

git clone git@github.com:jvehent/bigproject.git

Keep only the subdirectory for Project1

git filter-branch --prune-empty --subdirectory-filter Project1 -- --all