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(+)

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