Merge pull request #5473 from microDev1/patch

Allow any character except / in port or board name
This commit is contained in:
Jeff Epler 2021-10-25 16:54:27 -05:00 committed by GitHub
commit 9dea5ec724
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 2 deletions

View File

@ -62,8 +62,8 @@ def set_boards_to_build(build_all):
if not build_all: if not build_all:
boards_to_build = set() boards_to_build = set()
board_pattern = re.compile(r"^ports\/\w+\/boards\/(\w+)\/") board_pattern = re.compile(r"^ports\/[^/]+\/boards\/([^/]+)\/")
port_pattern = re.compile(r"^ports\/(\w+)\/") port_pattern = re.compile(r"^ports\/([^/]+)\/")
for p in changed_files: for p in changed_files:
# See if it is board specific # See if it is board specific
board_matches = board_pattern.search(p) board_matches = board_pattern.search(p)