Can't disable linter ?

Stream: lean4

[Arthur Adjedj]

Hi, I've come across what I believe to be a minor bug where disabling the unreachableTactic linter doesn't work:

set_option linter.unreachableTactic false in
notation "‹.›" => by assumption --this tactic is never executed [linter.unreachableTactic]

Despite seemingly turning off the linter option, I still get the linter message. Am I doing something wrong here ?

[Mario Carneiro]

Fixed on std master