Fix garbled filename output (#114)

This commit is contained in:
Kevin Wu 2020-05-07 13:07:47 -05:00 committed by GitHub
parent de9e9edc4d
commit 2625e178df
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 2 deletions

View File

@ -107,8 +107,8 @@ void outputCode(
// Start a separate process to redirect the model output. I/O redirection // Start a separate process to redirect the model output. I/O redirection
// changes will not be visible to the parent process. // changes will not be visible to the parent process.
if (fork() == 0) { if (fork() == 0) {
const char * tempFilename = (filename + extension).c_str(); string tempFilename = filename + extension;
freopen(tempFilename, "w", stderr); freopen(tempFilename.c_str(), "w", stderr);
module->dump(); module->dump();
fclose(stderr); fclose(stderr);
exit(0); exit(0);