diff options
| author | Hugo Herbelin | 2016-09-11 11:55:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-17 19:15:20 +0200 |
| commit | 94e8664074cfb987f8a63ca29c5436c861184b3a (patch) | |
| tree | ed520fdb1120c24fee4285e71ee73448d7d20c56 /kernel/nativecode.ml | |
| parent | 6d770156669dd9868ae7623b8f4302866e2cc8c7 (diff) | |
Stopping injection not to work on discriminable atoms (see #4890).
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions