From 3d2680a97a1ab9d85c4672217ec7957ce390bca1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 23 Jan 2017 22:25:57 +0100
Subject: [cosmetic] Reorder makefile as suggested by @herbelin

---
 Makefile.common | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Makefile.common b/Makefile.common
index 2c55d76cc..2cf4d0169 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -53,9 +53,9 @@ INSTALLSH:=./install.sh
 MKDIR:=install -d
 
 CORESRCDIRS:=\
-  config 	lib		kernel		kernel/byterun	library \
-  proofs 	tactics 	pretyping	interp		stm \
-  toplevel	parsing 	printing	intf	engine	ltac vernac
+  config 	lib		kernel	intf	kernel/byterun	library \
+  engine 	pretyping	interp	proofs	parsing 	printing \
+  tactics 	vernac		stm		toplevel 	ltac
 
 PLUGINDIRS:=\
   omega		romega 		micromega 	quote \
-- 
cgit v1.2.3