[develop] Replace manage_externals with Git submodules#1028
Draft
MichaelLueken wants to merge 24 commits into
Draft
[develop] Replace manage_externals with Git submodules#1028MichaelLueken wants to merge 24 commits into
MichaelLueken wants to merge 24 commits into