Does this work with spaces in the current directory, or do you need ` COQBIN="$(pwd)/coq-HoTT/bin"`? (Feel free to keep the backticks rather than using `$(pwd)`; I just don't know how to get them to render as backticks in Markdown without putting them on their own line.