On Thursday, October 05, 2017, Nicolas Pitre wrote: > Do you have the same amount of free memory once booted in both cases? Yes, almost exactly the same, so obvious it must be working the same for both cases. That's enough evidence for me. Thanks. Chris