diff options
Diffstat (limited to '020run.cc')
-rw-r--r-- | 020run.cc | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/020run.cc b/020run.cc index b94d274a..4d151b93 100644 --- a/020run.cc +++ b/020run.cc @@ -233,13 +233,11 @@ else if (is_equal(*arg, "--trace")) { :(code) void cleanup_main() { - if (Save_trace && Trace_stream) { - cerr << "writing trace to 'last_run'\n"; - ofstream fout("last_run"); - fout << Trace_stream->readable_contents(""); - fout.close(); - } - if (Trace_stream) delete Trace_stream, Trace_stream = NULL; + if (!Trace_stream) return; + if (Save_trace); + Trace_stream->dump(); + delete Trace_stream; + Trace_stream = NULL; } :(before "End One-time Setup") atexit(cleanup_main); |