Add missing docstrings

leanprover · Apr 5, 2024 · 6829f5e · 6829f5e
1 parent 0e1b1bf
commit 6829f5e
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/src/verso-manual/Verso/Genre/Manual/Basic.lean b/src/verso-manual/Verso/Genre/Manual/Basic.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import Lean
 import Verso.Doc
 import Verso.Doc.Html

diff --git a/src/verso-manual/Verso/Genre/Manual/Docstring.lean b/src/verso-manual/Verso/Genre/Manual/Docstring.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import Lean
 import Verso.Genre.Manual.Basic
 import Verso.Doc.Elab.Monad