Skip to content
This repository has been archived by the owner on Aug 29, 2023. It is now read-only.

Should leanproject get support branches? #21

Closed
gebner opened this issue Mar 6, 2020 · 1 comment
Closed

Should leanproject get support branches? #21

gebner opened this issue Mar 6, 2020 · 1 comment

Comments

@gebner
Copy link
Member

gebner commented Mar 6, 2020

I typically have one directory per mathlib branch, so it would be nice to get mathlib and immediately check out a given branch.

$ leanproject get mathlib:mon_loc
@PatrickMassot
Copy link
Member

Fixed in 4cbb34a.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@gebner @PatrickMassot