From d48dbccb0092550a69806402b02bc98a53f5f0bc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Sep 2014 18:07:54 -0700 Subject: [PATCH] fix(shell): allow multiple spaces after -D option Signed-off-by: Leonardo de Moura --- src/shell/lean.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 75f1b58ed..63c24f37a 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -155,6 +155,9 @@ public: }; options set_config_option(options const & opts, char const * in) { + if (!in) return opts; + while (*in && std::isspace(*in)) + ++in; std::string in_str(in); auto pos = in_str.find('='); if (pos == std::string::npos)