From 436abd92a520f13843b102b24b61802c88c7dba7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 15 Jun 2017 19:51:06 +0200
Subject: [make] remove compat5 file.

It is empty and not used anymore.
---
 tools/CoqMakefile.in | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index f1e519d038..e54ea45d41 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -182,7 +182,7 @@ else
 CAMLP4EXTEND=
 endif
 
-PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" compat5.cmo $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'
+PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'
 
 ifneq (,$(TIMING))
 TIMING_ARG=-time
-- 
cgit v1.2.3