diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 27dd560bc2..cf6c08e208 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -3,11 +3,19 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.DocString
 import Lean.Elab.Command
 import Lean.Elab.Open
 
 namespace Lean.Elab.Command
 
+@[builtinCommandElab moduleDoc] def elabModuleDoc : CommandElab := fun stx =>
+   match stx[1] with
+   | Syntax.atom _ val =>
+     let doc := val.extract 0 (val.bsize - 2)
+     modifyEnv fun env => addMainModuleDoc env doc
+   | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
+
 private def addScope (isNewNamespace : Bool) (header : String) (newNamespace : Name) : CommandElabM Unit := do
   modify fun s => { s with
     env    := s.env.registerNamespace newNamespace,