mathlib3
afae2c4b - doc(tactic/localized): unnecessary escape characters (#3322)

Commit

5 years ago

doc(tactic/localized): unnecessary escape characters (#3322) This is probably left over from when it was a string literal instead of a doc string.

Author

robertylewis

Parents