diff --git a/repos/ports/run/gdb_monitor.run b/repos/ports/run/gdb_monitor.run index defd62a6c..3066786dd 100644 --- a/repos/ports/run/gdb_monitor.run +++ b/repos/ports/run/gdb_monitor.run @@ -66,7 +66,7 @@ set config { - + @@ -74,7 +74,7 @@ set config { - + diff --git a/repos/ports/run/gdb_monitor_interactive.run b/repos/ports/run/gdb_monitor_interactive.run index cb397349a..bfeff4dcc 100644 --- a/repos/ports/run/gdb_monitor_interactive.run +++ b/repos/ports/run/gdb_monitor_interactive.run @@ -54,7 +54,7 @@ set config { - + @@ -62,7 +62,7 @@ set config { - +