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 c04480ef12..fcd6c81269 100644 --- a/Makefile.common +++ b/Makefile.common @@ -223,7 +223,7 @@ IDEMOD:=$(shell cat ide/ide.mllib) COQENVCMO:=$(CONFIG) \ lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \ - lib/util.cmo lib/system.cmo lib/envars.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) |