From 37938ecde1f8faf2beaffe05e7f85eb7118a9f78 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 11 Apr 2024 16:21:03 +0200
Subject: [PATCH] doc: moduleDoc (#3874)

---
 src/Lean/Parser/Command.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 6b4468c13e..ba24ca8f3b 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -44,6 +44,11 @@ match against a quotation in a command kind's elaborator). -/
 @[builtin_term_parser low] def quot := leading_parser
   "`(" >> withoutPosition (incQuotDepth (many1Unbox commandParser)) >> ")"
 
+/--
+`/-! <text> -/` defines a *module docstring* that can be displayed by documentation generation
+tools. The string is associated with the corresponding position in the file. It can be used
+multiple times in the same file.
+-/
 @[builtin_command_parser]
 def moduleDoc := leading_parser ppDedent <|
   "/-!" >> commentBody >> ppLine