17 Jun
2017
17 Jun
'17
7:35 p.m.
Le 17/06/2017 à 19:23, Tinu Weber a écrit :
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!
I’ve seen the deletion request indeed, but merged anyway. Merging transfer comments, votes and subscriptions to notifications from AUR users. Bruno