mathlib

462d96e5 - fix(scripts/add_port_comments): make message insertion less fragile (#17756)

fix(scripts/add_port_comments): make message insertion less fragile (#17756) This now doesn't make a mess of the whitespace. Previously it would put the `-/` on the same line as the blockquote, which while valid leads to bad highlighting in vscode and github. This also prevents mis-parsing caused by comments of the form `/-! /- -/ -/`