From 53ec9ee181d017ec30ce4bd3326a717c9e2efb3b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 14 May 2019 07:08:58 -0700
Subject: [PATCH] chore(*): style

---
 src/library/module.cpp | 3 ++-
 src/runtime/io.cpp     | 1 +
 src/runtime/io.h       | 1 +
 3 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/library/module.cpp b/src/library/module.cpp
index 72bfad1748..c7c1f08fde 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -110,11 +110,12 @@ extern "C" object * lean_read_module_data(object * fname, object * w) {
         if (size < header_size) {
             return set_io_error(w, (sstream() << "failed to read file '" << olean_fn << "', invalid header").str());
         }
-        char header[header_size];
+        char * header = new char[header_size];
         in.read(header, header_size);
         if (strncmp(header, g_olean_header, header_size) != 0) {
             return set_io_error(w, (sstream() << "failed to read file '" << olean_fn << "', invalid header").str());
         }
+        delete[] header;
         char * buffer = new char[size - header_size];
         in.read(buffer, size - header_size);
         if (!in) {
diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index 91274b0b3f..c03e5bf985 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <iostream>
 #include <chrono>
 #include <iomanip>
+#include <string>
 #include "runtime/object.h"
 #include "runtime/allocprof.h"
 namespace lean {
diff --git a/src/runtime/io.h b/src/runtime/io.h
index 6aea01a0a5..607ffd5f87 100644
--- a/src/runtime/io.h
+++ b/src/runtime/io.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <string>
 #include "runtime/object.h"
 namespace lean {
 obj_res set_io_result(obj_arg r, obj_arg a);