diff options
| author | Emilio Jesus Gallego Arias | 2018-12-10 14:08:56 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-10 14:08:56 +0100 |
| commit | 3f014b0c883cd71cf751b0ccc297edb38e46ae47 (patch) | |
| tree | cacc5fe6e908f7ba7ef1c99f0235da1f2876c7fa /.gitignore | |
| parent | 01f4470c330ce52b03046d5b98cd5af3ac87272e (diff) | |
| parent | e3a2a5d4fc3ad29462f2e4548c32ac00b4fbd05f (diff) | |
Merge PR #9077: Rename generated directory gramlib__pack -> gramlib/.pack
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/.gitignore b/.gitignore index da675309e5..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 @@ -178,3 +177,4 @@ theories/*/dune theories/*/*/dune theories/*/*/*/dune *.install +!Makefile.install |