From 9779c0bf4945693bfd37b141e2c9f0fea200ba4d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 25 Apr 2019 14:09:42 +0200
Subject: Integrate build and documentation of Ltac2

Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.

Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.
---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile')

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
-- 
cgit v1.2.3