## Stream: general

### Topic: system-wide elan

#### Patrick Massot (Jan 18 2019 at 09:33):

@Sebastian Ullrich I'd like to try to build a debian package for local deployment for my course. Is it possible to have a system-wide elan It seems elan always tries to install in the user directory

#### Patrick Massot (Jan 18 2019 at 09:33):

Or should I forget about elan and install Lean directly?

#### Sebastian Ullrich (Jan 18 2019 at 09:40):

You can do a system-wide installation of elan manually - here is Arch Linux's package for rustup for comparison: https://git.archlinux.org/svntogit/community.git/tree/trunk/PKGBUILD?h=packages/rustup#n30

#### Patrick Massot (Jan 18 2019 at 09:42):

Is there a command line argument for elan saying where it should install?

#### Sebastian Ullrich (Jan 18 2019 at 09:43):

But if you're using a single Lean version for your course, there's probably not much to benefit from elan

#### Patrick Massot (Jan 18 2019 at 09:44):

That's probably simpler indeed. Maybe releasing Lean 3.4.2 would also make it feel cleaner

#### Sebastian Ullrich (Jan 18 2019 at 09:45):

Yes, I hope I can get to that today

#### Patrick Massot (Jan 18 2019 at 09:45):

Thanks

Last updated: May 15 2021 at 00:39 UTC