1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 2b5d2cea16..c4404d13c7 100644
--- a/Makefile
+++ b/Makefile
@@ -66,7 +66,7 @@ FIND_SKIP_DIRS:='(' \
 ')' -prune -o
 
 define find
- $(shell find . $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||')
+ $(shell find . user-contrib/Ltac2 $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||')
 endef
 
 define findindir