From 35c28d8c506e1bb4d9b2f2afa6f2702aa359dc13 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 28 Aug 2018 13:03:43 +0200
Subject: Put camldevfiles targets in Makefile

There's no need to build dependencies for it.
---
 Makefile.dev | 16 +---------------
 1 file changed, 1 insertion(+), 15 deletions(-)

(limited to 'Makefile.dev')

diff --git a/Makefile.dev b/Makefile.dev
index ea1a3d40a2..68e96a57b7 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -15,7 +15,7 @@
 # Debug printers in dev/
 #########################
 
-.PHONY: devel printers camldevfiles
+.PHONY: devel printers
 
 DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo
 
@@ -85,20 +85,6 @@ endif
 # But these partial targets could be quite handy for quick builds
 # of specific components of Coq.
 
-###########################################################################
-# OCaml dev files
-###########################################################################
-camldevfiles: $(MERLINFILES) META.coq
-
-.merlin: .merlin.in
-	cp -a "$<" "$@"
-
-%/.merlin: %/.merlin.in
-	cp -a "$<" "$@"
-
-META.coq: META.coq.in
-	cp -a "$<" "$@"
-
 ###############################
 ### 1) general-purpose targets
 ###############################
-- 
cgit v1.2.3