diff options
| author | Hugo Herbelin | 2014-11-06 11:11:33 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-06 12:05:48 +0100 |
| commit | 6b2a56097a596638d2b297bd78534b2e7506e206 (patch) | |
| tree | 4e42556374b8e005c077140eb9559dd753451c5f /kernel/nativelib.ml | |
| parent | bc0cdb37c2117830f003a7fd8d87dbc12e4f085d (diff) | |
Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels)
by hopefully computing the right position where to reinit an empty
level. Also removing obsolete comment.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions