diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:14 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:14 +0200 |
| commit | da178a880e3ace820b41d38b191d3785b82991f5 (patch) | |
| tree | 6356ab3164a5ad629f4161dc6c44ead74edc2937 /Makefile.common | |
| parent | e4282ea99c664d8d58067bee199cbbcf881b60d5 (diff) | |
Imported Upstream version 8.2pl2+dfsgupstream/8.2.pl2+dfsg
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 d6f43cf5..4d76e9e5 100644 --- a/Makefile.common +++ b/Makefile.common @@ -435,7 +435,7 @@ MCHECKER:=\ # grammar modules with camlp4 GRAMMARNEEDEDCMO:=\ - lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \ + lib/profile.cmo lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \ lib/util.cmo lib/bigint.cmo lib/dyn.cmo lib/hashcons.cmo lib/predicate.cmo \ lib/rtree.cmo lib/option.cmo \ kernel/names.cmo kernel/univ.cmo \ |