From 0c139c895300be4f1842654c4aad089d5341a277 Mon Sep 17 00:00:00 2001 From: teorth Date: Thu, 9 Apr 2026 21:14:28 -0700 Subject: [PATCH] Remove pull request reference from CONTRIBUTING.md Removed a reference to a specific pull request in the CONTRIBUTING.md file. --- CONTRIBUTING.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index adc061a9..c5fc6db0 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -19,8 +19,6 @@ The Lean toolchain version is pinned in `lean-toolchain`. Mathlib is pinned in ` - **Line length.** Follow Mathlib convention: 100 characters max. - **Sorry warnings.** The project suppresses sorry warnings (`-Dwarn.sorry=false` in `lakefile.lean`) by design. -[#476]: https://github.com/teorth/analysis/pull/476 - ## Adding a section 1. Add the relevant file to `Analysis/`