Rename torproject-pusher to merge-bot
I keep getting confused when I need to find the "bot that does merging" here on Gitlab.
Any objections to renaming it to merge-bot
and maybe build a bit of precedence for Gitlab bots having a -bot
suffix?
From what I can tell, the bot is identified by its SSH key from git.torproject.org and thus the change is purely cosmetic here on Gitlab.
Let me know what you think :-)