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 /.merlin.in | |
| 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 '.merlin.in')
| -rw-r--r-- | .merlin.in | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/.merlin.in b/.merlin.in index db7259dd6f..4d646842d8 100644 --- a/.merlin.in +++ b/.merlin.in @@ -40,8 +40,8 @@ S API B API S ide B ide -S gramlib__pack -B gramlib__pack +S gramlib/.pack +B gramlib/.pack S tools B tools |