From 289c227ceac521f0bee95e2f0fa784ab319d49c6 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 8 Jul 2024 13:10:43 +0200 Subject: [PATCH] Fix manifest --- .github/workflows/push.yml | 1 + lake-manifest.json | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 0605b24..d0584f1 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -2,6 +2,7 @@ on: push: branches: - master + - gh-actions # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages permissions: diff --git a/lake-manifest.json b/lake-manifest.json index 97f4ee6..369eaca 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "38e09f6c5663173303181f2e3ac0c922f9f2eb2f", + "rev": "b387c548d1dc9cea5c5fcb71e5b3370cca1a04cc", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -101,5 +101,5 @@ "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}], - "name": "carleson", + "name": "bonnAnalysis", "lakeDir": ".lake"}