Zulip Chat Archive

Stream: general

Topic: leanpkg dependencies on branches

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?

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

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: Dec 20 2023 at 11:08 UTC