Revert weak args: this should build; then modify CI for archive

leanprover-community · Aug 5, 2024 · cf8847d · cf8847d
1 parent dfaf2f0
commit cf8847d
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 6 deletions.
diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean
@@ -220,7 +220,7 @@ end CDotLinter
 /-- The "longLine" linter emits a warning on lines longer than 100 characters.
 We allow lines containing URLs to be longer, though. -/
 register_option linter.longLine : Bool := {
-  defValue := true
+  defValue := false
   descr := "enable the longLine linter"
 }
 

diff --git a/lakefile.lean b/lakefile.lean
@@ -12,11 +12,7 @@ package mathlib where
   -- so they can be enabled in CI and disabled locally or vice versa.
   -- Warning: Do not put any options here that actually change the olean files,
   -- or inconsistent behavior may result
-  weakLeanArgs := #[
-    "linter.longLine true",
-    "linter.missingEnd true",
-    "linter.setOption true"
-  ]
+  -- weakLeanArgs := #[]
 
 /-!
 ## Mathlib dependencies on upstream projects.