diff options
author | Andrew Cagney <cagney@redhat.com> | 2004-07-26 19:01:36 +0000 |
---|---|---|
committer | Andrew Cagney <cagney@redhat.com> | 2004-07-26 19:01:36 +0000 |
commit | 2818e980840e9f4972f702d136ede4577a6a36f5 (patch) | |
tree | afebe5cc2bc186a08b31527ce6180bfd13b2edfa | |
parent | 5d0e1d25c8364a607322184b70ab322483148462 (diff) | |
download | gdb-2818e980840e9f4972f702d136ede4577a6a36f5.tar.gz |
2004-07-26 Andrew Cagney <cagney@gnu.org>
Problem reported by Ashley Pittman <ashley@quadrics.com>.
* main.c (captured_main): When in batch mode always detach.
-rw-r--r-- | gdb/main.c | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/gdb/main.c b/gdb/main.c index 4e5fd2a02f5..0042962c5dc 100644 --- a/gdb/main.c +++ b/gdb/main.c @@ -729,6 +729,13 @@ extern int gdbtk_test (char *); if (batch) { + if (attach_flag) + /* Either there was a problem executing the command in the + batch file aborted early, or the batch file forgot to do an + explicit detach. Explicitly detach the inferior ensuring + that there are no zombies. */ + target_detach (NULL, 0); + /* We have hit the end of the batch file. */ exit (0); } |