Join GitHub today
GitHub is home to over 36 million developers working together to host and review code, manage projects, and build software together.Sign up
Fixed missing pipe in ports page menu #10025
The ports page has a missing pipe in the menu between 'Update URL' and 'Search'.
DO NOT DELETE THIS TEXT
If you would like to test this pull request then please run: