chore: rename Std to Batteries (#11)

leanprover · May 13, 2024 · 5298d1b · 5298d1b
1 parent 8b3eddb
commit 5298d1b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/README.md b/README.md
@@ -42,7 +42,7 @@ jobs:
     mathlib-cache: ""
 
     # Run "lake exe runLinter" on the specified module.
-    # Project must be downstream of Std.
+    # Project must be downstream of Batteries.
     # Allowed values: name of module to lint.
     # If lint-module input is not provided, linter will not run.
     lint-module: ""

diff --git a/action.yml b/action.yml
@@ -6,7 +6,7 @@ description: |
     - get Mathlib cache (optional, must be downstream of Mathlib)
     - lake build
     - lake test (optional)
-    - lake exe runLinter (optional, must be downstream of Std)
+    - lake exe runLinter (optional, must be downstream of Batteries)
     - check reservoir eligibility (optional)
 inputs:
   test:
@@ -27,7 +27,7 @@ inputs:
   lint-module:
     description: |
       Run "lake exe runLinter" on the specified module.
-      Project must be downstream of Std.
+      Project must be downstream of Batteries.
       Allowed values: name of module to lint.
       If lint-module input is not provided, linter will not run.
     required: false