(main): Do not sync I/O streams with stdio, since I do not use stdin,

stdout or stderr.

1 files changed, 2 insertions, 0 deletions

diff --git a/main.cc b/main.cc
index 4dd2c9e5..bbfbdfab 100644
--- a/main.cc
+++ b/main.cc
@@ -539,6 +539,8 @@ def vmax(d, val):\n\
 
 int main(int argc, char * argv[], char * envp[])
 {
+  std::ios::sync_with_stdio(false);
+
   try {
     return parse_and_report(argc, argv, envp);
   }