diff options
| author | Guillaume Melquiond | 2015-10-29 17:22:08 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-10-29 17:22:08 +0100 |
| commit | 7f8a31e21edd533ba12399b7ee5647ef30e38fe5 (patch) | |
| tree | d9a4dd9c8b71b3df37e866b0b92a8ebbdf75a415 /kernel | |
| parent | dc13be3390c7b1d375d11842abb36e63aeb91cad (diff) | |
Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392)
Without this expansion, camlp4 fails to properly factor a user notation
starting with either "trivial" or "auto".
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions