mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 12:42:02 +03:00
Fix typo in bootstrap script
This commit is contained in:
parent
8fbce0cdc1
commit
d3fab2d28f
@ -31,4 +31,4 @@ make libs SCHEME=${SCHEME} PREFIX=${PREFIX}
|
||||
make install SCHEME=${SCHEME} PREFIX=${PREFIX}
|
||||
make clean IDRIS2_BOOT=${PREFIX}/bin/idris2sh
|
||||
make all IDRIS2_BOOT=${PREFIX}/bin/idris2sh SCHEME=${SCHEME} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
|
||||
make test INTERACTIVE='' LD_LIBRARY_PATH-${PREFIX}/lib IDRIS2_BOOT=${PREFIX}/bin/idris2sh SCHEME=${SCHEME} IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_LIBS=${PREFIX}/idris2-0.2.0/lib IDRIS2_DATA=${PREFIX}/idris2-0.2.0/support
|
||||
make test INTERACTIVE='' IDRIS2_BOOT=${PREFIX}/bin/idris2sh SCHEME=${SCHEME} IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_LIBS=${PREFIX}/idris2-0.2.0/lib IDRIS2_DATA=${PREFIX}/idris2-0.2.0/support
|
||||
|
Loading…
Reference in New Issue
Block a user