diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:17 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:17 +0200 |
commit | 2dad86a4e71bae9905b39970384328316e53eb42 (patch) | |
tree | 9fe7df673a3e36cfbee14f2a4afe5b5b6fc72e80 /Makefile.common | |
parent | 257f04de91e394cea67254da547fc1b90fa6978d (diff) | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Merge commit 'upstream/8.2pl2+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 \ |