There's a weird behavior of curl in PowerShell 5.1: when running the first command in the instructions, the created file is named --location instead of elan-init.ps1.
I checked that curl works properly in Command Prompt or PowerShell 7.4.1. To install elan, Windows users should use Command Prompt or PowerShell ≥ version 7.4.1.
There's a weird behavior of curl in PowerShell 5.1: when running the first command in the instructions, the created file is named
--location
instead ofelan-init.ps1
.I checked that curl works properly in Command Prompt or PowerShell 7.4.1. To install elan, Windows users should use Command Prompt or PowerShell ≥ version 7.4.1.
This pull request is a revision of https://github.com/leanprover/elan/pull/119. See also the discussion about this PR in the Lean Zulip chat.