diff --git a/runtime/src/main.c b/runtime/src/main.c index 795f2c5..a28eeab 100644 --- a/runtime/src/main.c +++ b/runtime/src/main.c @@ -182,9 +182,18 @@ runtime_start_runtime_worker_threads() debuglog("Sandboxing environment ready!\n"); } +void +runtime_cleanup() +{ + if (runtime_sandbox_perf_log != NULL) fflush(runtime_sandbox_perf_log); + + exit(EXIT_SUCCESS); +} + void runtime_configure() { + signal(SIGTERM, runtime_cleanup); /* Scheduler Policy */ char *scheduler_policy = getenv("SLEDGE_SCHEDULER"); if (scheduler_policy == NULL) scheduler_policy = "FIFO";