Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove Json module #84

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Remove Json module #84

wants to merge 1 commit into from

Conversation

dariusf
Copy link
Contributor

@dariusf dariusf commented Nov 18, 2022

Fixes #77. Got a conflict when modifying the Json module bundled with TLC locally, so finally got around to doing this.

@lemmy
Copy link
Member

lemmy commented Nov 18, 2022

I'm reluctant to merge this PR because it breaks users still on the latest 1.7.2. TLC release, which does not bundle Json.tla.

@dariusf
Copy link
Contributor Author

dariusf commented Nov 18, 2022

Ah. No worries, whenever is appropriate.

lemmy added a commit to tlaplus/tlaplus that referenced this pull request Feb 9, 2023
"The [Json] parser MAY silently ignore empty lines, e.g. \n\n".
https://github.com/ndjson/ndjson-spec#32-parsing

Corresponding commit in the CommunityModules:
tlaplus/CommunityModules@e17420d
(we maintain this fork because of
tlaplus/CommunityModules#84 (comment)

[Bug]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

Successfully merging this pull request may close these issues.

Remove Json module
2 participants