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

[ install ] Fix install-libdocs makefile target

Browse Source 
On some systems, `/bin/sh` is a symlink to a minimal shell (e.g. `dash`) that doesn't understand bashisms like `mkdir -p some_dir/{one,two,three}`.
This commit is contained in:
Kamil Shakirov 2021-09-16 17:12:01 +06:00 committed by G. Allais
parent 44328d73de
commit 304c0e666d
1 changed files with 5 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Makefile
View File

@ -209,7 +209,11 @@ install-with-src-libs:
${MAKE} -C libs/test install-with-src IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
install-libdocs: libdocs
mkdir -p ${PREFIX}/${NAME_VERSION}/docs/{prelude,base,contrib,network,test}
mkdir -p ${PREFIX}/${NAME_VERSION}/docs/prelude
mkdir -p ${PREFIX}/${NAME_VERSION}/docs/base
mkdir -p ${PREFIX}/${NAME_VERSION}/docs/contrib
mkdir -p ${PREFIX}/${NAME_VERSION}/docs/network
mkdir -p ${PREFIX}/${NAME_VERSION}/docs/test
cp -r libs/prelude/build/docs/* ${PREFIX}/${NAME_VERSION}/docs/prelude
cp -r libs/base/build/docs/* ${PREFIX}/${NAME_VERSION}/docs/base
cp -r libs/contrib/build/docs/* ${PREFIX}/${NAME_VERSION}/docs/contrib