Fix manifest

fpvandoorn · Jul 8, 2024 · 289c227 · 289c227
1 parent 2477ed7
commit 289c227
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git 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
@@ -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"}