idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 02:23:44 +03:00
Code Issues Projects Releases Wiki Activity

Add network to library search paths

Browse Source 
I don't know why this works for me locally but not on travis, although
it is harder for me to be sure this machine is completely clean! So the
easiest way to find out if this fixes the problem is probably just to
try it...
This commit is contained in:
Edwin Brady 2020-05-21 17:47:46 +01:00
parent 02ac3c9945
commit 492a6bc30f
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
bootstrap.sh
View File

@ -35,4 +35,4 @@ make clean IDRIS2_BOOT=${PREFIX}/bin/idris2
make all IDRIS2_BOOT=${PREFIX}/bin/idris2 SCHEME=${SCHEME} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
echo "Testing using libraries in ${IDRIS2_NEW_PATH}"
make test INTERACTIVE='' IDRIS2_PATH=${IDRIS2_NEW_PATH} SCHEME=${SCHEME} IDRIS2_LIBS=${PREFIX}/idris2-0.2.0/lib IDRIS2_DATA=${PREFIX}/idris2-0.2.0/support
make test INTERACTIVE='' IDRIS2_PATH=${IDRIS2_NEW_PATH} SCHEME=${SCHEME} IDRIS2_LIBS=${PREFIX}/idris2-0.2.0/lib:${PREFIX}/idris2-0.2.0/network/lib IDRIS2_DATA=${PREFIX}/idris2-0.2.0/support