As discussed in https://github.com/rust-bitcoin/rust-miniscript/pull/450#issuecomment-1253977283 the script currently warns about @ in PR description but it may be more convenient to jut remove them automatically. Not modifying the text sounds like a good default but having an option to just remove the symbols (possibly only those that really can be mentions) when one sees they are only mentions would be more convenient.
Yes i think this makes sense, if you can detect use that is definitely a github username, it could just remove the '@'. Currently maintainers do this manually.
As discussed in https://github.com/rust-bitcoin/rust-miniscript/pull/450#issuecomment-1253977283 the script currently warns about
@
in PR description but it may be more convenient to jut remove them automatically. Not modifying the text sounds like a good default but having an option to just remove the symbols (possibly only those that really can be mentions) when one sees they are only mentions would be more convenient.