Now that we're not hijacking the existing Jane Street libraries to extend them, there's very little difference between core_kernel_exts and base_exts, and it's probably best to delete the former until there are things in it that legitimately can't co-exist with base.
Now that we're not hijacking the existing Jane Street libraries to extend them, there's very little difference between
core_kernel_exts
andbase_exts
, and it's probably best to delete the former until there are things in it that legitimately can't co-exist with base.