Using a git submodule is relatively inconvienent for users. 1) One can easily forget cloning recursively leading to unexpected failure cases 2) It takes ages to clone the entire thing. I'd prefer if we copy the relevant files into the repo.
Using a git submodule is relatively inconvienent for users.
I'd prefer if we copy the relevant files into the repo.