I was unable to make changes to the existing pull request because I foolishly deleted
fork of the program. I am new to github. After some thought, I came to the conclusion that this is even good, since my changes in the patch are closely related to the existing debugger, and since the debugger, as I understand it, will be redone this year, there is no point improve the code that will stop working. I'll wait for the changes in the debugger ...