aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-07-03 16:00:22 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-07-10 20:25:10 +0200
commit475a3a6e48a9d5587be5281e5b2206f7c7c8946b (patch)
treecbc93a20b8e8429061703ec09c9459d201514889 /Makefile.common
parentb4572185522cd21e7e4e1cf59095ae66d0da0be1 (diff)
Compile coqpp inside the bin/ folder and make it available after installation.
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common3
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common
index 96d0d2ed8..fdaa94212 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -21,6 +21,7 @@ COQTOPEXE:=bin/coqtop$(EXE)
COQTOPBYTE:=bin/coqtop.byte$(EXE)
COQDEP:=bin/coqdep$(EXE)
+COQPP:=bin/coqpp$(EXE)
COQDEPBYTE:=bin/coqdep.byte$(EXE)
COQMAKEFILE:=bin/coq_makefile$(EXE)
COQMAKEFILEBYTE:=bin/coq_makefile.byte$(EXE)
@@ -40,7 +41,7 @@ COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py
COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py
TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
- $(COQWORKMGR)
+ $(COQWORKMGR) $(COQPP)
TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\
$(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES)