Done! Apparently the github magic button switches to dev automatically, so I acciedently made the changes on

dev

first, but I've now also added to

master

. Just be aware you may get a false-positive conflict or simething like that when merging