avaldebe
commented
8 years ago - create a branch with only the tools directory
git checkout -b tools master
git filter-branch --prune-empty --subdirectory-filter tools tools- create new remote branch and set the new branch to track it
git push -u origin tools
git branch --set-upstream-to=origin/tools tools- setup git-subtree at master
git checkout master
git rm -r tools/
git commit -m "move tools into own branch"
git subtree add --prefix=tools origin tools --squash
git subtree pull --prefix=tools origin tools -m "update subtree"
git push -u origin master
MAybe we should keep the tools in a separate branch/git-subtree, as it is done for source and docs