diff options
| author | Gaëtan Gilbert | 2020-02-25 13:45:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-25 13:45:22 +0100 |
| commit | f05348c7c809ad55316a3d9ae53b9b8640423978 (patch) | |
| tree | 3ea9aa7b766125ec399a34040785110b1d2df451 /kernel/nativecode.mli | |
| parent | 1bc8cd6390a3208659d563b1363f9bc0d87643a0 (diff) | |
| parent | 02b837e9b135fc828c8c8efc8eb1bc5b882f1aaf (diff) | |
Merge PR #11666: Do not perform a universe diff when typing opaque constants.
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions