aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorfilliatr2001-02-06 15:02:00 +0000
committerfilliatr2001-02-06 15:02:00 +0000
commit9c662cf9e8f4065ab354dc9c55c3e819f0db1fbe (patch)
treeb48820b8f0dea11a1156305c49a1f51e0f8effdc /Makefile
parent17ca87d5de9a232fc056c1bac85134094b03cd21 (diff)
mise en place extraction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1339 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile3
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 33a7321e9b..0f2323cb5b 100644
--- a/Makefile
+++ b/Makefile
@@ -31,7 +31,8 @@ noargument:
LOCALINCLUDES= -I config -I tools -I scripts -I lib -I kernel -I library \
-I proofs -I tactics -I pretyping -I parsing -I toplevel \
- -I contrib/omega -I contrib/ring -I contrib/xml
+ -I contrib/omega -I contrib/ring -I contrib/xml \
+ -I contrib/extraction
INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB)
BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG)