aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common
index 82d9b89c4f..415454df79 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -99,7 +99,7 @@ CORESRCDIRS:=\
coqpp \
config clib lib kernel kernel/byterun library \
engine pretyping interp proofs gramlib/.pack parsing printing \
- tactics vernac stm toplevel
+ tactics vernac stm sysinit toplevel
PLUGINDIRS:=\
omega micromega \
@@ -132,7 +132,7 @@ CORECMA:=config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/l
engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
gramlib/.pack/gramlib.cma \
parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
- stm/stm.cma toplevel/toplevel.cma
+ sysinit/sysinit.cma stm/stm.cma toplevel/toplevel.cma
###########################################################################
# plugins object files