mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 20:51:43 +03:00
Update INSTALL.md
make clean does a better job than just cleaning the build directories
This commit is contained in:
parent
bd6a4903b5
commit
9213b65ee1
@ -53,7 +53,7 @@ Then, go to the Self-hosting step below, but you'll also need to add
|
|||||||
`SCHEME=chez` (with the appropriate name for `chez`) so that the bootstrapping
|
`SCHEME=chez` (with the appropriate name for `chez`) so that the bootstrapping
|
||||||
script knows where to look. That is:
|
script knows where to look. That is:
|
||||||
|
|
||||||
* `rm -rf build` -- clean the build artefacts
|
* `make clean` -- clean the build artefacts
|
||||||
* `make all IDRIS2_BOOT=idris2sh SCHEME=chez`
|
* `make all IDRIS2_BOOT=idris2sh SCHEME=chez`
|
||||||
* `make install`
|
* `make install`
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user