MirrorMirror
/
riju
mirror of https://github.com/radian-software/riju.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Correctly chdir into Idris2 source dir

This commit is contained in:
Radon Rosborough 2020-10-05 07:33:15 -07:00
parent 01f93522bb
commit 08ff7edaa4
1 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
scripts/docker-install-phase6.bash
View File

@ -69,9 +69,11 @@ git clone https://github.com/m-ender/hexagony.git /opt/hexagony
# Idris # Idris
wget -nv https://www.idris-lang.org/idris2-src/idris2-latest.tgz wget -nv https://www.idris-lang.org/idris2-src/idris2-latest.tgz
tar -xf idris2-latest.tgz tar -xf idris2-latest.tgz
pushd Idris2-* >/dev/null
make bootstrap-build SCHEME=chezscheme PREFIX=/usr/local make bootstrap-build SCHEME=chezscheme PREFIX=/usr/local
make install PREFIX=/usr/local make install PREFIX=/usr/local
chmod -R a=u,go-w /usr/local/idris2-* chmod -R a=u,go-w /usr/local/idris2-*
popd >/dev/null
rm -rf Idris2-* idris2-latest.tgz rm -rf Idris2-* idris2-latest.tgz
# Kalyn # Kalyn