diff options
| author | Maxime Dénès | 2015-01-17 20:35:43 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-01-17 20:35:43 +0100 |
| commit | 4a96baf41965249c77b390dd252e8fa36b806c5f (patch) | |
| tree | e003fc27bdd641d3aa7414b92fd3c6c492e1cbf0 /kernel/nativevalues.ml | |
| parent | 5e5d51762df0e34769225e8c59c77b97b1212c29 (diff) | |
Fix #3379, now that Require inside modules is allowed again.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions