diff options
Diffstat (limited to 'tools/verification/rv/src/rv.c')
-rw-r--r-- | tools/verification/rv/src/rv.c | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/verification/rv/src/rv.c b/tools/verification/rv/src/rv.c index 239de054d1e0..b8fe24a87d97 100644 --- a/tools/verification/rv/src/rv.c +++ b/tools/verification/rv/src/rv.c @@ -191,6 +191,7 @@ int main(int argc, char **argv) * and exit. */ signal(SIGINT, stop_rv); + signal(SIGTERM, stop_rv); rv_mon(argc - 1, &argv[1]); } |