diff options
| author | Théo Zimmermann | 2019-05-07 13:41:04 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-07 13:41:04 +0200 |
| commit | 7602c2cb547fe6664f7a065d17717baf12b9da88 (patch) | |
| tree | 1b034b3646090d35a8d730cbec6a5cf1c91da804 /Makefile | |
| parent | 8aa64e7c4661549fef63a1c9c2e4e5284db911d8 (diff) | |
| parent | 9779c0bf4945693bfd37b141e2c9f0fea200ba4d (diff) | |
Merge PR #10002: Integrate ltac2
Ack-by: JasonGross
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: jfehrle
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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 |