mergeWithGrind and adaptation_note

Stream: mathlib4

[Chris Henson]

The mergeWithGrind linter currently triggers for

import Mathlib

set_option linter.tacticAnalysis.mergeWithGrind true

theorem foo : True := by
  #adaptation_note /-- -/
  grind

should this be added as an exception?

[Anne Baanen]

Definitely, I think we should skip it just like we would skip any comment.

[Chris Henson]

This has been added in #30803