Zulip Chat Archive

Stream: general

Topic: elan


view this post on Zulip Scott Morrison (Oct 10 2018 at 09:36):

What is the best way to create a new project folder, using a nightly version?

view this post on Zulip Scott Morrison (Oct 10 2018 at 09:36):

I found

elan run --install nightly-2018-08-23 leanpkg new my_playground

view this post on Zulip Scott Morrison (Oct 10 2018 at 09:36):

Is there anything simpler?

view this post on Zulip Gabriel Ebner (Oct 10 2018 at 09:40):

You could do leanpkg +nightly new my_playground.

view this post on Zulip Scott Morrison (Oct 10 2018 at 09:41):

Fantastic, thanks!


Last updated: May 16 2021 at 20:13 UTC