Add missing fetch command to lean3-source target

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4

Apache License 2.0

43 stars 15 forks source link

Add missing fetch command to lean3-source target #232

Closed Ruben-VandeVelde closed 1 year ago

Ruben-VandeVelde commented 1 year ago

Conflicts with #231

fpvandoorn commented 1 year ago

I came here to open a PR for this as well. I opened #244 which does this and more, so please merge at least one of these two PRs.

fpvandoorn commented 1 year ago

I think this is obsolete since #244 is merged. If @eric-wieser feels strongly, he can limit the git fetch that occurs twice in Makefile, but that should perhaps be a new PR.