chore: remove unused script

leanprover · Jan 4, 2025 · d27c5eb · d27c5eb
1 parent 158228e
commit d27c5eb
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 19 deletions.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -8,7 +8,7 @@ on:
 
 jobs:
   build:
-    name: batteries test build
+    name: doc-gen test build
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repo

diff --git a/test_docs.sh b/test_docs.sh