diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-03 16:00:22 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-10 20:25:10 +0200 |
commit | 475a3a6e48a9d5587be5281e5b2206f7c7c8946b (patch) | |
tree | cbc93a20b8e8429061703ec09c9459d201514889 /Makefile.common | |
parent | b4572185522cd21e7e4e1cf59095ae66d0da0be1 (diff) |
Compile coqpp inside the bin/ folder and make it available after installation.
Diffstat (limited to 'Makefile.common')
-rw-r--r-- | Makefile.common | 3 |
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) |