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.build | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.build')

diff --git a/Makefile.build b/Makefile.build
index 05633cecc8..c100eda400 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -64,7 +64,7 @@ AFTER ?=
 
 # build the different subsystems:
 
-world: camldevfiles coq coqide documentation revision
+world: coq coqide documentation revision
 
 coq: coqlib coqbinaries tools
 
-- 
cgit v1.2.3