Use https instead of git for fetching the standard library (#572)
* Use https instead of git for fetching the standard library * Clone the standard library shallowly
This commit is contained in:
parent
09d04baefd
commit
43bdaa94f4
1 changed files with 2 additions and 1 deletions
3
.gitmodules
vendored
3
.gitmodules
vendored
|
@ -1,3 +1,4 @@
|
|||
[submodule "standard-library"]
|
||||
path = standard-library
|
||||
url = git@github.com:agda/agda-stdlib.git
|
||||
url = https://github.com/agda/agda-stdlib.git
|
||||
shallow = true
|
||||
|
|
Loading…
Reference in a new issue