Use proper deprecation syntax

Author: grunweg

Mathlib/Tactic/Linter/Whitespace.lean

@@ -43,10 +43,10 @@ public register_option linter.style.whitespace : Bool := {
 }
 
 /-- Deprecated in favour of `linter.style.whitespace` -/
-@[deprecated linter.style.whitespace (since := "2026-01-07")]
 public register_option linter.style.commandStart : Bool := {
   defValue := false
   descr := "deprecated: use the `linter.style.whitespace` option instead"
+  deprecation? := some { since := "2026-01-07", text? := "use the `linter.style.whitespace` option instead" }
 }
 
 /-- If the `linter.style.whitespace.verbose` option is `true`, the `whitespace` linter

MathlibTest/Linter/Whitespace.lean

@@ -10,9 +10,16 @@ section
 
 set_option linter.style.setOption true
 
+/--
+warning: `linter.style.commandStart` has been deprecated: use the `linter.style.whitespace` option instead
+-/
 #guard_msgs in
 set_option linter.style.commandStart true
 
+/--
+warning: `linter.style.commandStart` has been deprecated: use the `linter.style.whitespace` option instead
+-/
+#guard_msgs in
 set_option linter.style.commandStart true in
 example : Nat := 0