diff options
| author | Maxime Dénès | 2016-09-15 16:57:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-01 17:19:17 +0200 |
| commit | 9d5b26370a530be4267d07c5bd6e7cf4618f0e4b (patch) | |
| tree | 39471ef6adc0edce4e76abe24ebb06e4e0c9a6d3 /kernel/nativelib.ml | |
| parent | cd0a6070d9627cdf335c4be0a03b9bbb81f7a738 (diff) | |
Remove allow_anonymous_refs.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions