Skip to content

chore: update ci#7810

Closed
oliveredget wants to merge 1 commit intocosmos:mainfrom
oliveredget:fix2
Closed

chore: update ci#7810
oliveredget wants to merge 1 commit intocosmos:mainfrom
oliveredget:fix2

Conversation

@oliveredget
Copy link
Contributor

I hope my corrections will help you. Thank you for your work.


Before we can merge this PR, please make sure that all the following items have been
checked off. If any of the checklist items are not applicable, please leave them but
write a little note why.

  • Targeted PR against the correct branch (see CONTRIBUTING.md).
  • Linked to GitHub issue with discussion and accepted design, OR link to spec that describes this work.
  • Code follows the module structure standards and Go style guide.
  • Wrote unit and integration tests.
  • Updated relevant documentation (docs/).
  • Added relevant godoc comments.
  • Provide a conventional commit message to follow the repository standards.
  • Include a descriptive changelog entry when appropriate. This may be left to the discretion of the PR reviewers. (e.g. chores should be omitted from changelog)
  • Re-reviewed Files changed in the GitHub PR explorer.
  • Review SonarCloud Report in the comment section below once CI passes.

Signed-off-by: oliveredget <188809800+oliveredget@users.noreply.github.com>
@gjermundgaraba
Copy link
Contributor

Hi @oliveredget. Thank you for the PR. We are not prioritizing fixing spelling mistakes in the .tla files until we have decided how to maintain those. So, for the time being I will close this PR.

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