diff options
| author | Emilio Jesus Gallego Arias | 2017-01-23 22:25:57 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-02-15 20:45:29 +0100 |
| commit | 3d2680a97a1ab9d85c4672217ec7957ce390bca1 (patch) | |
| tree | 9e16df937e23c01de3043b356d4aba9455912936 | |
| parent | fc6e78be83cef6e9b249ca146ef749ba90eb802c (diff) | |
[cosmetic] Reorder makefile as suggested by @herbelin
| -rw-r--r-- | Makefile.common | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Makefile.common b/Makefile.common index 2c55d76cc8..2cf4d01695 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 \ |