From 5b9b814fd1af96412ec482d945c045bd0c74d264 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Fri, 19 Sep 2014 09:35:32 -0700 Subject: [PATCH] fix(shell/lean.cpp): use binary mode to open cache file --- src/shell/lean.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 6d765218d..059960bf6 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -296,7 +296,7 @@ int main(int argc, char ** argv) { definition_cache * cache_ptr = nullptr; if (use_cache) { cache_ptr = &cache; - std::ifstream in(cache_name); + std::ifstream in(cache_name, std::ifstream::binary); if (!in.bad() && !in.fail()) cache.load(in); }