diff options
| author | coqbot-app[bot] | 2020-10-26 11:05:27 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-26 11:05:27 +0000 |
| commit | 9e7b0f9f248a1fae8e5681815bd621f182696c4f (patch) | |
| tree | 8de9102f30e1e9d2161d6a43e098ed9985e3a7d3 /kernel/nativecode.ml | |
| parent | 689e86b9241411180248e3115364a972833f0851 (diff) | |
| parent | a2ce4da4c2b0dc81d4c61f3e672d6c9d65dba46b (diff) | |
Merge PR #13257: adjust Search deprecation warning
Reviewed-by: Zimmi48
Reviewed-by: Blaisorblade
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions