aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-06-10 16:43:21 -0400
committerGravatar Jason Gross <jgross@mit.edu>2016-06-10 16:43:21 -0400
commit969cb56234750c320768ae39e934b18ce2883aef (patch)
tree50ceed23e66d66f635d671929f5330f52159defa /Makefile
parentecf5f6fc0d3107eeb8566f56037f28d888a53a1a (diff)
8.5 fixes
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 04df08ae3..5fb1ab33c 100644
--- a/Makefile
+++ b/Makefile
@@ -28,7 +28,7 @@ coqprime-8.5:
$(MAKE) -C coqprime-8.5
Makefile.coq: Makefile _CoqProject
- coq_makefile -f _CoqProject -o Makefile.coq
+ $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
clean: Makefile.coq
$(MAKE) -f Makefile.coq clean