From 08786611b8562cc84b5db9eada14cff88684af99 Mon Sep 17 00:00:00 2001 From: timechess Date: Sun, 8 Dec 2024 22:29:18 +0800 Subject: [PATCH] fix blueprint --- .github/workflows/build_blueprint.yml | 4 ++-- Makefile | 2 +- lakefile.lean | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/build_blueprint.yml b/.github/workflows/build_blueprint.yml index 0dac625..d5c2257 100644 --- a/.github/workflows/build_blueprint.yml +++ b/.github/workflows/build_blueprint.yml @@ -1,6 +1,6 @@ on: - push: - branches: [master] + workflow_dispatch: + jobs: build: permissions: diff --git a/Makefile b/Makefile index 191c90c..bf33a3d 100644 --- a/Makefile +++ b/Makefile @@ -20,7 +20,7 @@ build-web: (cd blueprint/src && poetry run plastex -c plastex.cfg web.tex) blueprint: build build-print build-web - (lake -Kenv=dev update doc-gen4 && lake -Kenv=dev build $(PROJECT):docs) + (lake -Kenv=dev update doc-gen4 -R && lake -Kenv=dev build $(PROJECT):docs) (cd blueprint && cp -r ../.lake/build/doc ./web/) blueprint-dev: build-print build-web diff --git a/lakefile.lean b/lakefile.lean index cea1db3..7de2065 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -19,4 +19,4 @@ lean_lib «RamificationGroup» where require local_class_field_theory from git "https://github.com/mariainesdff/LocalClassFieldTheory.git" meta if get_config? env = some "dev" then -- dev is so not everyone has to build it -require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "c7f4ac84b973b6efd8f24ba2b006cad1b32c9c53" +require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "v4.13.0"