From ed367a3c8a27de506f9f015f2798c8481a5b4565 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 15 Jun 2026 08:53:51 +0200 Subject: [PATCH] build exposition only on push --- .github/workflows/blueprint.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml index 5fc8ea56..42467d74 100644 --- a/.github/workflows/blueprint.yml +++ b/.github/workflows/blueprint.yml @@ -60,16 +60,19 @@ jobs: ./scripts/build_docs.sh - name: Clone lean-exposition + if: github.event_name == 'push' run: | git clone --depth 1 --branch "$LEAN_EXPOSITION_REF" \ "https://github.com/$LEAN_EXPOSITION_REPO" /tmp/lean-exposition - name: Build exposition binary + if: github.event_name == 'push' run: | cd /tmp/lean-exposition && lake build exposition echo "EXPOSITION_BIN=/tmp/lean-exposition/.lake/build/bin/exposition" >> "$GITHUB_ENV" - name: Build exposition documentation + if: github.event_name == 'push' run: | lake env "$EXPOSITION_BIN" \ --root LeanMachineLearning \