diff options
| author | Eelco Dolstra <edolstra@gmail.com> | 2018-12-12 13:20:59 +0100 |
|---|---|---|
| committer | Eelco Dolstra <edolstra@gmail.com> | 2019-02-11 12:05:17 +0100 |
| commit | dcae46ab146b735aa49fcf4cad4a320e79362c5e (patch) | |
| tree | d48ef2b512c2fe04992552282ca2d58d4242c127 /local.mk | |
| parent | ef4cf4e681bfe30b15b8c2940b51b322bce5b6d8 (diff) | |
Add github URIs
For example, github:edolstra/dwarffs is more-or-less equivalent to
https://github.com/edolstra/dwarffs.git. It's a much faster way to get
GitHub repositories: it fetches tarballs rather than entire Git
repositories. It also allows fetching specific revisions by hash
without specifying a ref (e.g. a branch name):
github:edolstra/dwarffs/41c0c1bf292ea3ac3858ff393b49ca1123dbd553
Diffstat (limited to 'local.mk')
0 files changed, 0 insertions, 0 deletions