aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile.build3
1 files changed, 1 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build
index ffe6a22490..bf5cdc5ada 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -65,8 +65,7 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \
-I contrib/interface -I contrib/fourier \
-I contrib/jprover -I contrib/cc \
-I contrib/funind -I contrib/firstorder \
- -I contrib/field -I contrib/subtac -I contrib/rtauto \
- -I contrib/recdef
+ -I contrib/field -I contrib/subtac -I contrib/rtauto
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)