Skip to content
New issue

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

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

Already on GitHub? # to your account

plutus exe doc: add some extra extensions #6789

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

Conversation

bezirg
Copy link
Contributor

@bezirg bezirg commented Jan 14, 2025

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

@bezirg bezirg self-assigned this Jan 14, 2025
@bezirg bezirg added the No Changelog Required Add this to skip the Changelog Check label Jan 14, 2025
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
No Changelog Required Add this to skip the Changelog Check
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant