110a111,127
>
> int remote_gdb_base_port = 7000;
>
> int
> getRemoteGDBPort()
> {
> return remote_gdb_base_port;
> }
>
> // Set remote GDB base port. 0 means disable remote GDB.
> // Callable from python.
> void
> setRemoteGDBPort(int port)
> {
> remote_gdb_base_port = port;
> }
>