Hi, On Fri, Dec 29, 2023 at 02:51:31PM +0100, Luca Dariz wrote: > > > + $ gdb gnuamch > > > > Typo ;) > > What would be a better command? This is actually how I start gdb from the > build directory,
You probably start gnumach though, and not gnuamch? Michael