(the debugging options refer to debugging of user code rather than tools)