When trying to install sirdi using make install, I get the following error:
install build/exec/sirdi ~/.idris2/bin
install: cannot create regular file '/home/thomas/.idris2/bin': No such file or directory
make: *** [Makefile:23: install] Error 1
I have PREFIX set to ${HOME}/.idris2-git to avoid confusion with the latest release build and that's probably what's causing this error. It would be neat if sirdi took PREFIX into account : )
When trying to install sirdi using
make install, I get the following error:I have
PREFIXset to${HOME}/.idris2-gitto avoid confusion with the latest release build and that's probably what's causing this error. It would be neat if sirdi tookPREFIXinto account : )