diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-05 14:24:08 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-05 14:24:08 -0500 |
| commit | de3346f052111a23ada2687af7a8b52150faec4a (patch) | |
| tree | c93ad2fcfcbb8737ba91ef7857cdac444b4501e7 /Makefile | |
| parent | c07e8d7dd27750737d80c35d0eec124ae48196d9 (diff) | |
Replace $(shell pwd) with ${CURDIR}
On Cygwin, `$(shell pwd)` gives a Linux path (`/cygdrive/...`), which
is wrong. We now use `${CURDIR}`, as per
http://stackoverflow.com/a/3679235.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -75,7 +75,7 @@ endif endif endif -COQPATH?=$(shell pwd)/$(COQPRIME_FOLDER) +COQPATH?=${CURDIR}/$(COQPRIME_FOLDER) export COQPATH coqprime: |