diff options
| author | Gaëtan Gilbert | 2018-08-28 13:03:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-08-28 13:03:43 +0200 |
| commit | 35c28d8c506e1bb4d9b2f2afa6f2702aa359dc13 (patch) | |
| tree | 204a2458b21dca908a34e625c6cefa711c053703 /Makefile.build | |
| parent | f885e8a88620351d9dc4b0969f520d13197f2184 (diff) | |
Put camldevfiles targets in Makefile
There's no need to build dependencies for it.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
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 |