Skip to content

Refactor and add SyntheticSources - #60

Merged
tesujimath merged 2 commits into
mainfrom
synthetic-sources
Apr 8, 2026
Merged

Refactor and add SyntheticSources#60
tesujimath merged 2 commits into
mainfrom
synthetic-sources

Conversation

@tesujimath

Copy link
Copy Markdown
Owner

SyntheticSources allow for error reports to refer to text which doesn't occur in the original sources.

The motivation for this is to support plugins, which may create mew directives, and these ought to be
able to be the subject of error reports.

@tesujimath
tesujimath merged commit 988c459 into main Apr 8, 2026
4 checks passed
@tesujimath
tesujimath deleted the synthetic-sources branch April 8, 2026 21:31
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