diff options
| author | Emilio Jesus Gallego Arias | 2018-10-06 17:54:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-29 01:25:21 +0100 |
| commit | 06979f87959866e6ed1214e745893dcd2e8ddbb3 (patch) | |
| tree | 458274f8a8afedc314535db28e0936b7fe3bec3c /Makefile | |
| parent | 665146168720c094ce4fbb3d7d044d9904099f95 (diff) | |
[gramlib] Original Import from Camlp5 repos.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -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 \ |