aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
authorMaxime Dénès2017-12-14 00:06:02 +0100
committerMaxime Dénès2017-12-14 00:06:02 +0100
commit290abf59e6f13bb1468d8e3df050cf0bd9c48708 (patch)
treea61d3dce0bd34372b48668f44d280b5d886e2994 /Makefile.common
parent7576ffd4eb196d5d5a15f6cacb2ba5cba00576ef (diff)
parentf5cb7eb3e68e4b7d1bb5eeb8d9c58666201945d4 (diff)
Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common2
1 files changed, 0 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common
index 4d63b08e2b..f436d3e8f1 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -12,8 +12,6 @@
# Executables
###########################################################################
-COQMKTOP:=bin/coqmktop$(EXE)
-
COQTOPBYTE:=bin/coqtop.byte$(EXE)
COQTOPEXE:=bin/coqtop$(EXE)