Hello! l...@gnu.org (Ludovic Courtès) writes:
> This is the potentially controversial patch. :-) > > It removes serverboot, which is no longer built since commit > dfa4d617a012dd46d3849e0d2538a4b7890c1306 (Sept. 2004), and moves the > files that are actually used by ‘mach-defpager’ in ‘mach-defpager/’. > > As a side effect, it fixes “make dist” in ‘mach-defpager’. Just friendly reminder that this patch is pending review. Ludo’.