Skip to content

Commit 40bb95d

Browse files
chabulhwiKha
authored andcommitted
doc: clarify installation instructions for Windows
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.
1 parent 640358e commit 40bb95d

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ Lean (version 4.0.0-nightly-2023-06-27, commit bb8cc08de85f, Release)
3737
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
3838
```
3939

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

0 commit comments

Comments
 (0)