mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 01:09:03 +03:00
Add note to INSTALL.md re: PREFIX being an absolute path
This commit is contained in:
parent
722bab8110
commit
da21f0477a
@ -34,7 +34,7 @@ of `make` in the following steps.
|
||||
|
||||
### 1: Set installation target directory
|
||||
|
||||
- Change the `PREFIX` in `config.mk`. The default is to install in
|
||||
- Change the `PREFIX` in `config.mk` to the absolute path of your chosen installation destination. The default is to install in
|
||||
`$HOME/.idris2`
|
||||
|
||||
If you have an existing Idris 2, go to Step 3. Otherwise, read on...
|
||||
|
Loading…
Reference in New Issue
Block a user