Time Nick Message 07:30 sfan5 alternatively curl -Ls PR_URL.patch | git am - 07:31 sfan5 or git fetch origin pull/NUMBER/merge && git merge --no-edit FETCH_HEAD 21:38 MTDiscord rubenwardy: for my add server favorite button PR, do I need the make it so it highlights the now favorited server, or fix the bug where it doesn't select a server anymore, and you can unfavorite a server that isn't even favorited? 21:39 rubenwardy Former - when you favourite or unfavourite a server, it should maintain the selection 21:39 MTDiscord hmm 21:40 MTDiscord I figured out how to fix the bug, but the highlighting part might be interesting to figure out. 21:40 rubenwardy could you store the selection by address/port and find the index based on that? 21:40 MTDiscord if I can figure it out...should I fix it for delting favorites too? 21:41 rubenwardy should just work if you do that 21:41 MTDiscord so I just need to get the index again? 21:54 MTDiscord currently index is found by using core.get_table_index 21:54 MTDiscord hmm