Merge pull request #1574 from I-B-3/patch-1

Add clarifying note re: PREFIX in config.mk
idris-lang · Jun 23, 2021 · 0a0c41d · 0a0c41d
2 parents c1057a1 + da21f04
commit 0a0c41d
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/INSTALL.md b/INSTALL.md
@@ -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...

diff --git a/config.mk b/config.mk
@@ -1,6 +1,6 @@
 ##### Options which a user might set before building go here #####
 
-# Where to install idris2 binaries and libraries
+# Where to install idris2 binaries and libraries (must be an absolute path)
 PREFIX ?= $(HOME)/.idris2
 
 # For Windows targets. Set to 1 to support Windows 7.