-
Oswald Buddenhagen authored
this is where it belongs, rather than into some arbitrary editor. as a nice side effect, now not only the "rename symbol", but also the global search&replace has such a warning.
a14955d0
this is where it belongs, rather than into some arbitrary editor. as a nice side effect, now not only the "rename symbol", but also the global search&replace has such a warning.