Runing elan-init.sh under msys2 makes elan available via cmd, but not via msys2.

[kim-em]

The elan-init.sh script doesn't work as I would have expected when run inside msys2. It installs everything (and sets up the PATH) in the Windows home directory C:\Users\scott\.elan, rather than the msys2 home directory C:\msys64\home\scott\.elan.

As a consequence (even after restarting msys2, lean isn't found.

This isn't terrible, just unexpected?

[kim-em]

(Our mathlib3 instructions for windows currently advise against using msys2, and instead using git bash, so presumably this hasn't been affecting people.)

[Kha]

I think the installation location is fine, but it would be nice if it also updated the msys2 shells. Not sure if msys2 sets any environment variables we could use to detect that and locate /etc.