Skip to content

Removing not used deferred_logger#6747

Merged
daavid00 merged 1 commit into
OPM:masterfrom
daavid00:warn
Jan 22, 2026
Merged

Removing not used deferred_logger#6747
daavid00 merged 1 commit into
OPM:masterfrom
daavid00:warn

Conversation

@daavid00
Copy link
Copy Markdown
Member

Removing not used deferred_logger

@daavid00 daavid00 added the manual:irrelevant This PR is a minor fix and should not appear in the manual label Jan 22, 2026
@daavid00
Copy link
Copy Markdown
Member Author

jenkins build this please

Copy link
Copy Markdown
Member

@GitPaean GitPaean left a comment

Choose a reason for hiding this comment

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

It looks good to me. Can be merged after jenkins approves.

@daavid00 daavid00 merged commit 42a94df into OPM:master Jan 22, 2026
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

manual:irrelevant This PR is a minor fix and should not appear in the manual

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants