diff options
| author | Gaëtan Gilbert | 2018-11-26 15:04:09 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-06 15:13:49 +0100 |
| commit | e3a2a5d4fc3ad29462f2e4548c32ac00b4fbd05f (patch) | |
| tree | 4470538f3e0862f4b503882416162aafb2e47879 /.gitignore | |
| parent | f3a7d021e6b347c2c0edf3c07f3206f22dcdf39a (diff) | |
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.
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 3 |
1 files changed, 1 insertions, 2 deletions
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 |