Skip to content

fix build with -DUSE_OPM_COMMON=OFF#1016

Merged
bska merged 1 commit into
OPM:masterfrom
akva2:fix_build_no_common
Apr 7, 2026
Merged

fix build with -DUSE_OPM_COMMON=OFF#1016
bska merged 1 commit into
OPM:masterfrom
akva2:fix_build_no_common

Conversation

@akva2
Copy link
Copy Markdown
Member

@akva2 akva2 commented Apr 7, 2026

No description provided.

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

akva2 commented Apr 7, 2026

jenkins build this please

Copy link
Copy Markdown
Member

@bska bska left a comment

Choose a reason for hiding this comment

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

Very good. I'll merge into master.

@bska bska merged commit 4d41332 into OPM:master Apr 7, 2026
3 checks passed
@akva2 akva2 deleted the fix_build_no_common branch April 7, 2026 07:59
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