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.

Sign up for GitHub

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

Jump to bottom

Remove annotation from Version #5148

Merged
merged 1 commit into from
Feb 15, 2023
Merged

Remove annotation from Version #5148

merged 1 commit into from
Feb 15, 2023

Conversation

michaelpj
Copy link
Contributor

It's not useful, we don't need a position for it or any other kind of
annotation really.

Pre-submit checklist:

  • Branch
    • Tests are provided (if possible)
    • Commit sequence broadly makes sense
    • Key commits have useful messages
    • Changelog fragments have been written (if appropriate)
    • Relevant tickets are mentioned in commit messages
    • Formatting, PNG optimization, etc. are updated
  • PR
    • (For external contributions) Corresponding issue exists and is linked in the description
    • Targeting master unless this is a cherry-pick backport
    • Self-reviewed the diff
    • Useful pull request description
    • Reviewer requested

@michaelpj
Remove annotation from Version
2104cd3 
It's not useful, we don't need a position for it or any other kind of
annotation really.
@michaelpj
Copy link
Contributor Author

I think this is probably uncontroversial.

@michaelpj michaelpj merged commit 48c326a into master Feb 15, 2023
@michaelpj michaelpj deleted the mpj/no-ann-version branch February 15, 2023 14:29
@bezirg
Copy link
Contributor

bezirg commented Feb 16, 2023

Note to future selves: this changes the Flat encoding of annotated Terms, but does not change the Flat encoding of empty-annotated Terms (Term () , etc) which are on the chain.

v0d1ch pushed a commit to v0d1ch/plutus that referenced this pull request Dec 6, 2024
@michaelpj @v0d1ch
Remove annotation from Version (IntersectMBO#5148)
680ffde 
It's not useful, we don't need a position for it or any other kind of
annotation really.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@michaelpj @bezirg