Closed ziyuwan closed 5 months ago
For example, I'd like to know whether just copying the
~/.elan
to the target machine can solve this problem.
Yes, that should work. Depending on your needs, it might also be easier to just deploy and use Lean without elan.
Thanks for your reply. I will close this issue currently.
Hi~ I'm trying to install
elan
and some required versions of lean package on a machine that do not have access to the Internet.So I would appreciate it if there were some ways to install
elan
offline.For example, I'd like to know whether just copying the
~/.elan
to the target machine can solve this problem.Could you please give me any instructions?