From 06979f87959866e6ed1214e745893dcd2e8ddbb3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 6 Oct 2018 17:54:24 +0200
Subject: [gramlib] Original Import from Camlp5 repos.

---
 Makefile | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 9ac32625ab..f2dc6d7750 100644
--- a/Makefile
+++ b/Makefile
@@ -57,6 +57,7 @@ FIND_SKIP_DIRS:='(' \
   -name '_build' -o \
   -name '_build_ci' -o \
   -name '_install_ci' -o \
+  -name 'gramlib' -o \
   -name 'user-contrib' -o \
   -name 'test-suite' -o \
   -name '.opamcache' -o \
-- 
cgit v1.2.3