Merge master into nightly-testing

leanprover-community · Nov 24, 2024 · 804dcc2 · 804dcc2
2 parents 64e861c + 3ece930
commit 804dcc2
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean
@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
--- First import Aesop and Qq
+-- First import Aesop, Qq, and Plausible
 import Aesop
 import Qq
+import Plausible
 
 -- Tools for analysing imports, like `#find_home`, `#minimize_imports`, ...
 import ImportGraph.Imports

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4a0cc9424af7acd48ce2e156e1257b718ccb79cf",
+   "rev": "85cadff63aab36f19c18434921628449ab540bd6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",