aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-06-19 15:38:21 -0400
committerGravatar Jason Gross <jgross@mit.edu>2018-06-19 15:38:21 -0400
commitf64e618b4f101f2c0dd2d66425673165bd60a785 (patch)
tree7140ba316618b5fcc14ecbe5e3af0553c243b207 /Makefile
parentac80a94132cab53c40638bbea6843c0d84c15645 (diff)
Make COQPATH in Makefile work on Windows / cygwin
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile8
1 files changed, 7 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 8981cfe23..9dfbb75c3 100644
--- a/Makefile
+++ b/Makefile
@@ -232,7 +232,13 @@ endif
OTHERFLAGS += -w "-notation-overridden"
endif
-COQPATH?=${CURDIR}/$(COQPRIME_FOLDER)/src
+ifneq ($(filter /cygdrive/%,$(CURDIR)),)
+CURDIR_SAFE := $(shell cygpath -m "$(CURDIR)")
+else
+CURDIR_SAFE := $(CURDIR)
+endif
+
+COQPATH?=${CURDIR_SAFE}/$(COQPRIME_FOLDER)/src
export COQPATH
coqprime: