Skip to content

Feature: add option to change port#11

Open
btrem wants to merge 3 commits intomicroformats:mainfrom
btrem:add_change_port_option
Open

Feature: add option to change port#11
btrem wants to merge 3 commits intomicroformats:mainfrom
btrem:add_change_port_option

Conversation

@btrem
Copy link

@btrem btrem commented Dec 9, 2022

Allows user to change the port of the dev
server by adding -p or --port= on the command
line.

Allows user to change the port of the dev
server by adding -p or --port= on the command
line.
@btrem
Copy link
Author

btrem commented Dec 9, 2022

NB: I'm pretty novice when it comes to Python. So review carefully! ;-)

btrem added 2 commits December 9, 2022 12:33
Shorter dest name makes help text more readable.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant