diff options
| author | Vincent Laporte | 2018-10-24 11:42:01 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-24 11:54:31 +0000 |
| commit | bcf64b062a1dde1e2322e84cb041607bf76b0b78 (patch) | |
| tree | 8cecbaea107911d76e8ea971bab1b03c59ef3995 /kernel/nativevalues.ml | |
| parent | a546d298a32e5000ef3f318b68924648adf1eb8a (diff) | |
[Manual] Avoid using deprecated “Focus”
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions