aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorfilliatr1999-08-16 14:01:48 +0000
committerfilliatr1999-08-16 14:01:48 +0000
commit3bb8e20dcabb74363315db5f85f9f8ba4ceb768f (patch)
tree381e10b43f5a9c53815583bf93945046f6efefa6 /Makefile
parentb4a932fad873357ebe50bf571858e9fca842b9e5 (diff)
ancien names decoupe en names + sign
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile5
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index cb3d0b2a9f..091cd578cd 100644
--- a/Makefile
+++ b/Makefile
@@ -11,19 +11,20 @@ noargument:
@echo " make cleanall"
@echo or make archclean
-INCLUDES=-I config -I lib
BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG)
OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF)
OCAMLDEP=ocamldep
DEPFLAGS=$(INCLUDES)
+INCLUDES=-I config -I lib -I kernel
+
# Objects files
CONFIG=config/coq_config.cmo
LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/hashcons.cmo
-KERNEL=kernel/names.cmo
+KERNEL=kernel/names.cmo kernel/sign.cmo
OBJS=$(CONFIG) $(LIB) $(KERNEL)