fix(server): update server url when the port change - #210
Conversation
cf15a27 to
34d8701
Compare
There was a problem hiding this comment.
Pull request overview
Fixes a local-server retry bug in language_tool_python where, after switching to a different port due to a startup failure, the client continued sending requests to the original (now incorrect) server URL.
Changes:
- Update
LanguageTool._urlwhenever_start_server_on_free_port()switches to a new port after aServerError. - Document the fix in
CHANGELOG.mdunder Unreleased → Fixed.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.
| File | Description |
|---|---|
src/language_tool_python/server.py |
Keeps _url in sync with _port when retrying local server startup on a new port. |
CHANGELOG.md |
Adds an Unreleased “Fixed” entry describing the corrected port/URL mismatch behavior. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
|
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## master #210 +/- ##
==========================================
- Coverage 80.70% 80.65% -0.05%
==========================================
Files 13 13
Lines 1767 1768 +1
==========================================
Hits 1426 1426
- Misses 341 342 +1 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
fix(server): update server url when the port change
Why the pull request was made
Because actually, when the server port change, we don't change the server url, and the healthcheck test to ensure that the server is alive will fail.
Summary of changes
LanguageTool._urlwhen we need to change the starting port.Screenshots (if appropriate):
Not applicable.
Applied local tests.
Resources
Not applicable.
Types of changes
Checklist