Improved UX for editing labels in GUI#966

tturocy wants to merge 4 commits into

mastergambitproject/gambit:masterfrom

issue_945gambitproject/gambit:issue_945Copy head branch name to clipboard