Allow port numbers to be used in local host names. e.g. localhost:8888 #6448
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
allow ports to be used in host names. e.g. localhost:8888. Note: code copied from pull request 5318, #5318. I did not test this.
Background
There are scenarios where local development or specific server configurations require non-standard ports to be used in conjunction with hostnames such as localhost. The current implementation of check_local_file_access does not allow for URLs with such ports, making it inconvenient or impossible for developers and users to utilize the software in some local environments. This pull request updates the function to be more accommodating to such URLs, enhancing the tool's flexibility.
Changes 🏗️
Modified the check_local_file_access function in to accommodate URLs with ports in host names.
Removed redundant entries in the local_prefixes list.
PR Quality Scorecard ✨
+2 pts
+5 pts
+5 pts
+5 pts
-4 pts
+4 pts
+5 pts
-5 pts
agbenchmark
to verify that these changes do not regress performance?+10 pts