diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index 18f7e8b04..c27dd84ac 100644 --- a/Makefile.common +++ b/Makefile.common @@ -233,7 +233,7 @@ IDEMOD:=$(shell cat ide/ide.mllib) COQENVCMO:=$(CONFIG) \ lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \ - lib/segmenttree.cmo lib/unicodetable.cmo lib/util.cmo lib/system.cmo \ + lib/segmenttree.cmo lib/unicodetable.cmo lib/util.cmo lib/errors.cmo lib/system.cmo \ lib/envars.cmo COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo |