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 /kernel/cbytecodes.mli | |
| 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 'kernel/cbytecodes.mli')
0 files changed, 0 insertions, 0 deletions