diff options
| author | Emilio Jesus Gallego Arias | 2020-02-12 23:12:26 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-13 22:11:05 +0100 |
| commit | 8d73861eeae56321a106f28d07b47d5d6699939d (patch) | |
| tree | 31e8ee4a328798a9269141dab30c77e70b78bdfd /Makefile.common | |
| parent | 4ea2825a4589b0c77225dd6f4caf98b12ac6dd6f (diff) | |
[coqdep] Remove support for `-c` ocamldep replacement.
There is not need for coqdep to ship an `ocamldep` replacement, in
particular:
- not used in the main build since a long time
- not tested
- not kept up to date with upstream
This allows for a significant reduction of `coqdep` code, including
some duplicated code from `ocamllibdep`.
`coq_makefile` now uses `ocamllibdep` to process `mllib/mlpack` files,
so it has then to be installed.
We also remove the residual `-slash` option.
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Makefile.common b/Makefile.common index 32bf19e99c..780ba717ee 100644 --- a/Makefile.common +++ b/Makefile.common @@ -42,17 +42,17 @@ COQTIME_FILE_MAKER:=tools/TimeFileMaker.py COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py VOTOUR:=bin/votour +OCAMLLIBDEP:=bin/ocamllibdep$(EXE) +OCAMLLIBDEPBYTE:=bin/ocamllibdep.byte$(EXE) # these get installed! TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ - $(COQWORKMGR) $(COQPP) $(VOTOUR) + $(COQWORKMGR) $(COQPP) $(VOTOUR) $(OCAMLLIBDEP) TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\ $(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES) COQDEPBOOT:=bin/coqdep_boot$(EXE) COQDEPBOOTBYTE:=bin/coqdep_boot.byte$(EXE) -OCAMLLIBDEP:=bin/ocamllibdep$(EXE) -OCAMLLIBDEPBYTE:=bin/ocamllibdep.byte$(EXE) FAKEIDE:=bin/fake_ide$(EXE) FAKEIDEBYTE:=bin/fake_ide.byte$(EXE) |