From f3a7d021e6b347c2c0edf3c07f3206f22dcdf39a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Dec 2018 14:58:15 +0100
Subject: unignore Makefile.install

Relevant for gitignore aware tools like ag (silversearcher)
---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)

(limited to '.gitignore')

diff --git a/.gitignore b/.gitignore
index da675309e5..8b81037a14 100644
--- a/.gitignore
+++ b/.gitignore
@@ -178,3 +178,4 @@ theories/*/dune
 theories/*/*/dune
 theories/*/*/*/dune
 *.install
+!Makefile.install
-- 
cgit v1.2.3


From e3a2a5d4fc3ad29462f2e4548c32ac00b4fbd05f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 26 Nov 2018 15:04:09 +0100
Subject: Rename generated directory gramlib__pack -> gramlib/.pack

It's a bit cleaner this way, especially wrt the number of toplevel directories.

Also fix warning about undefined GRAMMARCMA while we're at it.
---
 .gitignore | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to '.gitignore')

diff --git a/.gitignore b/.gitignore
index 8b81037a14..0411247abf 100644
--- a/.gitignore
+++ b/.gitignore
@@ -165,8 +165,7 @@ user-contrib
 plugins/ssr/ssrparser.ml
 plugins/ssr/ssrvernac.ml
 
-# gramlib__pack
-gramlib__pack
+/gramlib/.pack
 
 # ocaml dev files
 .merlin
-- 
cgit v1.2.3