Renaming lean projects

Stream: general

[Ben Eltschig]

I've set up a lean project a while ago that I would like to rename - my goals with the project have shifted a lot, and I don't think its name accurately reflects its contents anymore. Is there an easy / recommended way to do this, like a lake command? Currently the only two options I can think of are:

1. go through the entire repository and search for mentions of the project name, then replace them
2. create a new lake project, then copy the lean files over

Is that what I should do? Or is there anything I should be aware of, or that could make this process easier?

[Yury G. Kudryashov]

You can do (1) with one repository-wide search&replace (+some git moves).