Skip to content

Get named-character JSON from scanner rather than create a local copy.#1707

Merged
rocky merged 3 commits intomasterfrom
use-scanner-JSON-tables
Mar 3, 2026
Merged

Get named-character JSON from scanner rather than create a local copy.#1707
rocky merged 3 commits intomasterfrom
use-scanner-JSON-tables

Conversation

@rocky
Copy link
Member

@rocky rocky commented Mar 3, 2026

Get named-character JSON from scanner rather than create a local copy.

rather than create a local copy.
@rocky rocky requested a review from mmatera March 3, 2026 02:27
@mmatera
Copy link
Contributor

mmatera commented Mar 3, 2026

LGTM

@rocky rocky merged commit eb3135b into master Mar 3, 2026
21 checks passed
@rocky rocky deleted the use-scanner-JSON-tables branch March 3, 2026 22:05
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.

2 participants