aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common5
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common
index fcd6c81269..a1bfd08856 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -156,7 +156,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \
CORECMA:=lib/lib.cma kernel/kernel.cma library/library.cma \
pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \
- parsing/highparsing.cma tactics/hightactics.cma
+ parsing/highparsing.cma tactics/hightactics.cma
OMEGACMA:=plugins/omega/omega_plugin.cma
ROMEGACMA:=plugins/romega/romega_plugin.cma
@@ -223,7 +223,8 @@ IDEMOD:=$(shell cat ide/ide.mllib)
COQENVCMO:=$(CONFIG) \
lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \
- lib/unicodetable.cmo lib/util.cmo lib/system.cmo lib/envars.cmo
+ lib/segmenttree.cmo lib/unicodetable.cmo lib/util.cmo lib/system.cmo \
+ lib/envars.cmo
COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo
COQMKTOPCMX:=$(COQMKTOPCMO:.cmo=.cmx)