Re: [aur-requests] Package rename: epfl-menu → epfl-menu-git

On Sat, Jun 17, 2017 at 19:10:30 +0200, Bruno Pagani wrote:

And since you’ve already pushed the right version, I did the merge. ;)

Ah yes, I created the new repository after asking here, but then I made a deletion request rather than a merge request (I'm not quite sure what exactly a merge does, though...) Thank you!