mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-29 14:44:03 +03:00
Try to fix bootstrap script
I think the tests are using the libraries from the bootstrap Idris 2, not the just built Idris 2, so if the ttc formats aren't idential the tests won't work. Let's see if that theory is correct...
This commit is contained in:
parent
bd093e9cba
commit
4ed38bd47d
@ -31,4 +31,4 @@ make libs SCHEME=${SCHEME} PREFIX=${PREFIX}
|
||||
make install SCHEME=${SCHEME} PREFIX=${PREFIX}
|
||||
make clean IDRIS2_BOOT=${PREFIX}/bin/idris2
|
||||
make all IDRIS2_BOOT=${PREFIX}/bin/idris2 SCHEME=${SCHEME} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
|
||||
make test INTERACTIVE='' IDRIS2_BOOT=${PREFIX}/bin/idris2 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/idris2 SCHEME=${SCHEME} IDRIS2_LIBS=${PREFIX}/idris2-0.2.0/lib IDRIS2_DATA=${PREFIX}/idris2-0.2.0/support
|
||||
|
Loading…
Reference in New Issue
Block a user