Skip to content

Schedule daily CI run#833

Merged
tpazderka merged 2 commits intomasterfrom
schedule-ci
Nov 17, 2022
Merged

Schedule daily CI run#833
tpazderka merged 2 commits intomasterfrom
schedule-ci

Conversation

@tpazderka
Copy link
Collaborator

  • Any changes relevant to users are recorded in the CHANGELOG.md.
  • The documentation has been updated, if necessary.
  • New code is annotated.
  • Changes are covered by tests.

@tpazderka tpazderka requested a review from schlenk November 17, 2022 17:18
Copy link
Collaborator

@schlenk schlenk left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM.

Should help with tools/checkers breaking over time.

@tpazderka tpazderka merged commit 083ac78 into master Nov 17, 2022
@tpazderka tpazderka deleted the schedule-ci branch November 17, 2022 17:57
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