diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 0f7edc7180..954337709c 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -83,7 +83,7 @@ declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant»
 @[builtinCommandParser] def printAxioms    := parser! "#print " >> nonReservedSymbol "axioms " >> ident
 @[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident
 @[builtinCommandParser] def «init_quot»    := parser! "init_quot"
-@[builtinCommandParser] def «set_option»   := parser! "set_option " >> ident >> (nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit)
+@[builtinCommandParser] def «set_option»   := parser! "set_option " >> ident >> ppSpace >> (nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit)
 @[builtinCommandParser] def «attribute»    := parser! "attribute " >> "[" >> sepBy1 Term.attrInstance ", " >> "] " >> many1 ident
 @[builtinCommandParser] def «export»       := parser! "export " >> ident >> "(" >> many1 ident >> ")"
 def openHiding       := parser! atomic (ident >> "hiding") >> many1 ident