Skip to content

Remove weird @

Robbert Krebbers requested to merge robbert/weird_at_sign into master

I noticed this while reviewing !931 (merged). It seems like a no-op.

Merge request reports