Closed rgrinberg closed 11 years ago
Thanks! Did not see the pull request!! I think I really have to do something about sorting my github mails. In the meantine, @yallop made a one line fix that is supposed to fix the issue, can you check if the new version is working now (also updated in opam). If it works, then I think @yallop solution is nicer.
No problem, @yallop's fix is cleaner. Works for me btw.
make install did not actually work for me with zsh. I think because of the brace expansion (it would not be expanded). I've made a fix to use pure make and not rely on any bashisms.