mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-24 06:52:19 +03:00
[ doc ] Fix prefix var, IDRIS2_PREFIX
is used, not PREFIX
This commit is contained in:
parent
14f2196d15
commit
9d93e74012
@ -126,7 +126,7 @@ Given an Idris package file ``test.ipkg`` it can be used with the Idris compiler
|
||||
+ ``idris2 --build test.ipkg`` will build all modules in the package
|
||||
|
||||
+ ``idris2 --install test.ipkg`` will install the package to the global
|
||||
Idris library directory (that is ``$PREFIX/idris-<version>/``),
|
||||
Idris library directory (that is ``$IDRIS2_PREFIX/idris-<version>/``),
|
||||
making the modules in its ``modules`` field accessible by other Idris
|
||||
libraries and programs. Note that this doesn't install any executables, just
|
||||
library modules.
|
||||
@ -148,7 +148,7 @@ Where does Idris look for packages?
|
||||
Compiled packages are directories with compiled TTC files (see :ref:`build-artefacts` section).
|
||||
Directory structure of the source `*.idr` files is preserved for TTC files.
|
||||
|
||||
Compiled packages can be installed globally (under ``$PREFIX/idris-<version>/`` as
|
||||
Compiled packages can be installed globally (under ``$IDRIS2_PREFIX/idris-<version>/`` as
|
||||
described above) or locally (under a ``depends`` subdirectory in the top level
|
||||
working directory of a project).
|
||||
Packages specified using ``-p pkgname`` or with the ``depends`` field of a
|
||||
@ -157,7 +157,7 @@ package will then be located as follows:
|
||||
* First, Idris looks in ``depends/pkgname-<version>``, for a package which
|
||||
satisfies the version constraint.
|
||||
* If no package is found locally, Idris looks in
|
||||
``$PREFIX/idris-<version>/pkgname-<version>``.
|
||||
``$IDRIS2_PREFIX/idris-<version>/pkgname-<version>``.
|
||||
|
||||
In each case, if more than one version satisfies the constraint, it will choose
|
||||
the one with the highest version number.
|
||||
|
@ -52,9 +52,9 @@ Once you've successfully bootstrapped with any of the above commands, you can
|
||||
install with the command ``make install``. This will, by default, install into
|
||||
``${HOME}/.idris2``. You can change this by editing the options in
|
||||
``config.mk``. For example, to install into ``/usr/local``, you can edit the
|
||||
``PREFIX`` as follows::
|
||||
``IDRIS2_PREFIX`` as follows::
|
||||
|
||||
PREFIX ?= /usr/local
|
||||
IDRIS2_PREFIX ?= /usr/local
|
||||
|
||||
Installing from a Package Manager
|
||||
=================================
|
||||
|
Loading…
Reference in New Issue
Block a user