Making Lean project a git submodule of another git repo

[kevinsullivan]

It would be lovely if instructions could be given for accomplishing this task. We want a lean project that we're developing, which uses mathlib, to be a git subproject of a larger git repo that we're developing. We want to be able to update lean and mathlib using these tools, while pushing changes to our own code to our own repo.

[semorrison]

I do this all the time. I just `git submodule add` the project, and then use leanproject inside that directory as usual.

…

On Mon, Mar 30, 2020 at 5:26 AM Kevin Sullivan ***@***.***> wrote: It would be lovely if instructions could be given for accomplishing this task. We want a lean project that we're developing, which uses mathlib, to be a git subproject of a larger git repo that we're developing. We want to be able to update lean and mathlib using these tools, while pushing changes to our own code to our own repo. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#37>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AADUWBHRXQOBKEFLLBUSM4TRJ6HDZANCNFSM4LWCIMUA> .

[PatrickMassot]

Thanks for you contribution. We are closing all pull requests and issues since this tool no longer has any relevance in the Lean 4 era. This repository will now be archived.