Closed beeshot closed 4 years ago
Hm, isn't this the same as #19? Better to start new branch for new work.
So if I look into the commit history, this branch looks a bit weird, with merging against the changes of #19 etc. So better to delete it I assume?
It is always better if a new PR comes from a new branch, else GitHub will get confused (and the user will also get confused ^^).
fixed vertex & label size