diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-23 22:25:57 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-15 20:45:29 +0100 |
commit | 3d2680a97a1ab9d85c4672217ec7957ce390bca1 (patch) | |
tree | 9e16df937e23c01de3043b356d4aba9455912936 /Makefile.common | |
parent | fc6e78be83cef6e9b249ca146ef749ba90eb802c (diff) |
[cosmetic] Reorder makefile as suggested by @herbelin
Diffstat (limited to 'Makefile.common')
-rw-r--r-- | Makefile.common | 6 |
1 files 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 \ |