aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
authorMaxime Dénès2019-02-04 13:05:00 +0100
committerMaxime Dénès2019-02-04 13:05:00 +0100
commit129d47518ae950c6ef1b69763e93cd70c14863f6 (patch)
treee5ae9646636c50f07c3b60e08eccb76e5b6eff96 /Makefile.common
parent0be49a49c41e28b2015440723882e0ca15c02d5e (diff)
parent103f59ed6b8174ed9359cb11c909f1b2219390c9 (diff)
Merge PR #8690: [toplevel] Split interactive toplevel and compiler binaries.
Reviewed-by: maximedenes Ack-by: ppedrot
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.common b/Makefile.common
index 2dced04967..f998ea867b 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -32,6 +32,7 @@ COQWCBYTE:=bin/coqwc.byte$(EXE)
COQDOC:=bin/coqdoc$(EXE)
COQDOCBYTE:=bin/coqdoc.byte$(EXE)
COQC:=bin/coqc$(EXE)
+COQCOPT:=bin/coqc.opt$(EXE)
COQCBYTE:=bin/coqc.byte$(EXE)
COQWORKMGR:=bin/coqworkmgr$(EXE)
COQWORKMGRBYTE:=bin/coqworkmgr.byte$(EXE)