From 88023e959796ec9b504f47b901556ef95fc76e2e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Apr 2015 14:23:01 -0700 Subject: [PATCH] fix(shell/lean): missing 'break' --- src/shell/lean.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index a351d6b813..d621ac80aa 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -392,6 +392,7 @@ int main(int argc, char ** argv) { case 'i': index_name = optarg; gen_index = true; + break; case 'M': lean::set_max_memory_megabyte(atoi(optarg)); opts = opts.update(lean::get_max_memory_opt_name(), atoi(optarg));