From 8d73861eeae56321a106f28d07b47d5d6699939d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 12 Feb 2020 23:12:26 +0100
Subject: [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.
---
 Makefile.common | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Makefile.common')

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)
 
-- 
cgit v1.2.3