From fbe1e685d3ba6dc75d8095369e0a98d4e77b8f4f Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Fri, 15 Dec 2023 14:45:22 -0700
Subject: [PATCH] Load doc-gen4 as a git dependency.

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

diff --git a/.gitmodules b/.gitmodules
deleted file mode 100644
index 13ef051..0000000
--- a/.gitmodules
+++ /dev/null
@@ -1,3 +0,0 @@
-[submodule "doc-gen4"]
-	path = doc-gen4
-	url = git@github.com:jrpotter/bookshelf-doc.git
diff --git a/doc-gen4 b/doc-gen4
deleted file mode 160000
index d2db077..0000000
--- a/doc-gen4
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit d2db077fc447a918d90a4515d8fb77d41dd79e42
diff --git a/lake-manifest.json b/lake-manifest.json
index 0d00acf..40bd115 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -82,11 +82,14 @@
    "inputRev": "doc-gen",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"type": "path",
+  {"url": "https://github.com/jrpotter/bookshelf-doc",
+   "type": "git",
+   "subDir": null,
+   "rev": "c29c914910af31f82e73cc0ab77d918a6439fb80",
    "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 755e1e7..de5d007 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -10,8 +10,9 @@ require mathlib from git
 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 "./doc-gen4"
+require «doc-gen4» from git
+  "https://github.com/jrpotter/bookshelf-doc" @
+    "main"
 
 @[default_target]
 lean_lib «Bookshelf» {