From de1405afd3c0ac316c54a9e55b14d8dbd6c52392 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 11 Aug 2022 23:49:30 +0200
Subject: [PATCH] fix: pipeline for new build

---
 .github/workflows/build.yml | 8 --------
 deploy_docs.sh              | 2 +-
 2 files changed, 1 insertion(+), 9 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index ba1ad2f..8f961d9 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -25,14 +25,6 @@ jobs:
         run: |
           lake build
 
-      - name: Checkout and compile LeanInk
-        run: |
-          cd ../
-          git clone https://github.com/hargonix/LeanInk
-          cd LeanInk
-          git checkout doc-gen
-          lake build
-
       - name: Checkout and compile mathlib4
         run: |
           cd ../
diff --git a/deploy_docs.sh b/deploy_docs.sh
index 3eec3b8..6042795 100755
--- a/deploy_docs.sh
+++ b/deploy_docs.sh
@@ -23,7 +23,7 @@ fi
 
 # generate the docs
 cd $1
-../$2/build/bin/doc-gen4 --ink ../$4/build/bin/leanInk Mathlib
+lake -Kenv=dev build Mathlib:docs --verbose
 
 if [ "$3" = "true" ]; then
   cd ..