changing default directory for lake, lean, and elan

Stream: lean4

[Jordi Majó]

Hello,

I am trying to install elan with the elan.init.ps1 script, but I would need to change the installation directory because the default directory in Windows (in my case) is "c:\Users\Jordi Majó", and the "ó" creates problems to install Mathlib later on.

Does anyone know a way to tell the elan installer not to use the defauld directory and use a different one?

Thanks

[Eric Wieser]

the default directory in Windows (in my case) is "c:\Users\Jordi Majó", and the "ó" creates problems to install Mathlib later on.

Do you have a thread somewhere about these problems?

[Jordi Majó]

I just opened it