From 024a298eb7b11fffa6ac3c742124671a1a2e5140 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 13 Sep 2022 19:11:13 +0200
Subject: [PATCH] chore: use new constructor docstring syntax

---
 Lake/Config/Glob.lean       | 12 ++++++------
 Lake/Config/LeanConfig.lean | 16 ++++++++--------
 2 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/Lake/Config/Glob.lean b/Lake/Config/Glob.lean
index ceb503d17d..fb920434a2 100644
--- a/Lake/Config/Glob.lean
+++ b/Lake/Config/Glob.lean
@@ -13,12 +13,12 @@ namespace Lake
 
 /-- A specification of a set of module names. -/
 inductive Glob
-| /-- Selects just the specified module name. -/
-  one : Name → Glob
-| /-- Selects all submodules of the specified module, but not the module itself. -/
-  submodules : Name → Glob
-| /-- Selects the specified module and all submodules. -/
-  andSubmodules : Name → Glob
+  /-- Selects just the specified module name. -/
+  | one : Name → Glob
+  /-- Selects all submodules of the specified module, but not the module itself. -/
+  | submodules : Name → Glob
+  /-- Selects the specified module and all submodules. -/
+  | andSubmodules : Name → Glob
 deriving Inhabited, Repr
 
 instance : Coe Name Glob := ⟨Glob.one⟩
diff --git a/Lake/Config/LeanConfig.lean b/Lake/Config/LeanConfig.lean
index 0c1b40c53a..6110a01560 100644
--- a/Lake/Config/LeanConfig.lean
+++ b/Lake/Config/LeanConfig.lean
@@ -10,28 +10,28 @@ Lake equivalent of CMake's
 [`CMAKE_BUILD_TYPE`](https://stackoverflow.com/a/59314670).
 -/
 inductive BuildType
-| /--
+  /--
   Debug optimization, asserts enabled, custom debug code enabled, and
   debug info included in executable (so you can step through the code with a
   debugger and have address to source-file:line-number translation).
   For example, passes `-Og -g` when compiling C code.
   -/
-  debug
-| /--
+  | debug
+  /--
   Optimized, *with* debug info, but no debug code or asserts
   (e.g., passes `-O3 -g -DNDEBUG` when compiling C code).
   -/
-  relWithDebInfo
-| /--
+  | relWithDebInfo
+  /--
   Same as `release` but optimizing for size rather than speed
   (e.g., passes `-Os -DNDEBUG` when compiling C code).
   -/
-  minSizeRel
-| /--
+  | minSizeRel
+  /--
   High optimization level and no debug info, code, or asserts
   (e.g., passes `-O3 -DNDEBUG` when compiling C code).
   -/
-  release
+  | release
 deriving Inhabited, Repr, DecidableEq, Ord
 
 instance : LT BuildType := ltOfOrd