From f76457cd6f560cf42fd32d1e25e02a532d87b824 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Thu, 14 Dec 2023 15:24:10 -0700
Subject: [PATCH] Now point to doc-gen4 fork.

---
 .gitmodules        | 3 +++
 doc-gen4           | 1 +
 lake-manifest.json | 7 ++-----
 lakefile.lean      | 3 +--
 4 files changed, 7 insertions(+), 7 deletions(-)
 create mode 100644 .gitmodules
 create mode 160000 doc-gen4

diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 0000000..13ef051
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "doc-gen4"]
+	path = doc-gen4
+	url = git@github.com:jrpotter/bookshelf-doc.git
diff --git a/doc-gen4 b/doc-gen4
new file mode 160000
index 0000000..86d5c21
--- /dev/null
+++ b/doc-gen4
@@ -0,0 +1 @@
+Subproject commit 86d5c219a9ad7aa686c9e0e704af030e203c63a1
diff --git a/lake-manifest.json b/lake-manifest.json
index f777383..0d00acf 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -82,14 +82,11 @@
    "inputRev": "doc-gen",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4",
-   "type": "git",
-   "subDir": null,
-   "rev": "86d5c219a9ad7aa686c9e0e704af030e203c63a1",
+  {"type": "path",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
    "inherited": false,
+   "dir": "././doc-gen4",
    "configFile": "lakefile.lean"}],
  "name": "bookshelf",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 39a8fc4..755e1e7 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -11,8 +11,7 @@ require std from git
   "https://github.com/leanprover/std4.git" @
     "v4.3.0"
 meta if get_config? env = some "dev" then
-  require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @
-    "main"
+  require «doc-gen4» from "./doc-gen4"
 
 @[default_target]
 lean_lib «Bookshelf» {