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

Change boot directory

Browse Source
This commit is contained in:
Edwin Brady 2020-05-18 16:23:37 +01:00
parent 9619c4aaae
commit 2ef0dec192
2 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

0
bootstrap/idris2-boot_app/idris2sh.ss → bootstrap/idris2sh_app/idris2sh.ss
View File

2
init-bootstrap
View File

@ -5,7 +5,7 @@ cp support/c/$IDRIS2_SUPPORT bootstrap/idris2-boot_app
cd bootstrap
sed s/libidris2_support.so/$IDRIS2_SUPPORT/g idris2-boot_app/idris2sh.ss > idris2-boot_app/idris2-boot.ss
sed s/libidris2_support.so/$IDRIS2_SUPPORT/g idris2sh_app/idris2sh.ss > idris2sh_app/idris2-boot.ss
${SCHEME} --script compile.ss
mkdir -p ../build/exec