Zulip Chat Archive

Stream: general

Topic: leanpkg dependencies on branches


view this post on Zulip Scott Morrison (May 13 2018 at 11:43):

I'd like to add a leanpkg dependency to a non-master branch of a github. Does anyone know how to do this?

view this post on Zulip Simon Hudon (May 13 2018 at 20:35):

On github, get the commit hash of the head of that branch and paste it leanpkg.toml

view this post on Zulip Scott Morrison (May 13 2018 at 23:16):

Okay -- I discovered the same thing in the meantime, but leanpkg upgrade then takes me off that branch back to master, which is not ideal, although certainly manageable.


Last updated: May 15 2021 at 22:14 UTC