diff options
| author | Gaëtan Gilbert | 2018-12-06 14:58:15 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-06 15:13:49 +0100 |
| commit | f3a7d021e6b347c2c0edf3c07f3206f22dcdf39a (patch) | |
| tree | 88dd1ac2265b6c9b912e91a0ba911cb6a4edcab2 /.gitignore | |
| parent | a2c8b7df8a0702ab716c0b97ad63d235b58b93a0 (diff) | |
unignore Makefile.install
Relevant for gitignore aware tools like ag (silversearcher)
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
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 |