summaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-01 17:21:17 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-01 17:21:17 +0200
commit2dad86a4e71bae9905b39970384328316e53eb42 (patch)
tree9fe7df673a3e36cfbee14f2a4afe5b5b6fc72e80 /Makefile.common
parent257f04de91e394cea67254da547fc1b90fa6978d (diff)
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Merge commit 'upstream/8.2pl2+dfsg'
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common2
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 \