Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
I've also modified the vendor script slightly so that we do a more efficient "git clone" by simply fetch the commit we want straight from the remote and checking it out locally. Downloading opam takes a long time, so I think this is a good idea. We can eventually consolidate a lot of the common funcitons in the vendor update scripts and do the same everywhere. Signed-off-by: Ali Caglayan <alizter@gmail.com>
- Loading branch information