diff --git a/.github/workflows/build_book.yml b/.github/workflows/build_book.yml index f76a1990..37916bc1 100644 --- a/.github/workflows/build_book.yml +++ b/.github/workflows/build_book.yml @@ -49,7 +49,7 @@ jobs: - name: Build book run: | - ~/.elan/bin/lake exe analysis-book + ~/.elan/bin/lake exe analysis-book --docgen-url "https://teorth.github.io/analysis/docs/" - name: Copy docs to analysis-book run: | cp -r ../analysis/.lake/build/doc _site/docs diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index a65ab7ec..ad60cb18 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -13,7 +13,7 @@ lake exe Analysis:docs Change the working directory to `./book/` Build: ``` -lake exe analysis-book +lake exe analysis-book --docgen-url "http://localhost:8000/analysis/docs/" ``` View the book: diff --git a/README.md b/README.md index b104ffa8..3e375474 100644 --- a/README.md +++ b/README.md @@ -107,8 +107,9 @@ To build the project's web page after [installing Lean](https://www.lean-lang.or % lake build % cd ../ % cd book/ -% lake exe analysis-book +% lake exe analysis-book --docgen-url="" % cd ../ ``` +where `` is `http://localhost:8000/analysis/docs` for the local setup. After this, `book/_site/` contains the project's web page. diff --git a/book/lake-manifest.json b/book/lake-manifest.json index badbb86b..802745e6 100644 --- a/book/lake-manifest.json +++ b/book/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "56d79b34f49586d95ac0a7c3d71f1342469d025d", + "rev": "36c5e5f804a3e3af661f550380628b037dcd5b08", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "analysis",