Skip to content

Commit

Permalink
doc: clarify installation instructions for Windows
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
chabulhwi authored and Kha committed Feb 1, 2024
1 parent 640358e commit 40bb95d
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ Lean (version 4.0.0-nightly-2023-06-27, commit bb8cc08de85f, Release)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
```

**Windows**: run the following commands in a terminal:
**Windows**: run the following commands in a terminal (Command Prompt or PowerShell ≥ version 7.4.1):
```bash
curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
powershell -ExecutionPolicy Bypass -f elan-init.ps1
Expand Down

0 comments on commit 40bb95d

Please sign in to comment.