diff options
| author | Hugo Herbelin | 2014-11-06 12:29:01 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-06 12:29:20 +0100 |
| commit | 01be85dd34c59fb0f410e10dc86979fe7a5c583f (patch) | |
| tree | d9782e30807a7de41ae5fb790ac95dcd6b5221b7 /kernel | |
| parent | 6b2a56097a596638d2b297bd78534b2e7506e206 (diff) | |
Test for bug #3723 and #3787 on reinitialization of empty camlp4/5 levels.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions