Browse Source

Set floating-point precision to 10 digits for file export

tempestpy_adaptions
Matthias Volk 5 years ago
parent
commit
ee3c08a085
  1. 1
      src/storm/utility/file.h

1
src/storm/utility/file.h

@ -22,6 +22,7 @@ namespace storm {
filestream.open(filepath); filestream.open(filepath);
} }
STORM_LOG_THROW(filestream, storm::exceptions::FileIoException , "Could not open file " << filepath << "."); STORM_LOG_THROW(filestream, storm::exceptions::FileIoException , "Could not open file " << filepath << ".");
filestream.precision(10);
if (!silent) { if (!silent) {
STORM_PRINT_AND_LOG("Write to file " << filepath << "." << std::endl); STORM_PRINT_AND_LOG("Write to file " << filepath << "." << std::endl);
} }

Loading…
Cancel
Save