diff options
| author | Maxime Dénès | 2015-10-14 16:40:53 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-10-14 16:41:57 +0200 |
| commit | db80daaf82a08a1475c65f7c82bffb63c7efd27a (patch) | |
| tree | 7434552be2f13b230c4e27a865ddfeb154355aa5 /kernel/indtypes.ml | |
| parent | 36f669f769fa23eb897adfa0450875a3c0db3476 (diff) | |
Temporary fix: kernel conversion needs to ignore l2r flag.
Stdlib does not compile when l2r flag is actually taken into account. We should
investigate...
Diffstat (limited to 'kernel/indtypes.ml')
0 files changed, 0 insertions, 0 deletions