Skip to content

Conversation

@Yadunund
Copy link
Member

We should do a normal merge commit for this instead of a squash.

 Signed-off-by: Esteban Martinena <[email protected]>
@Yadunund
Copy link
Member Author

@luca-della-vedova can you enable "merge commits" for this repo temporarily to merge this in?

@Yadunund
Copy link
Member Author

On second thought, it should be fine to squash merge this in.

@Yadunund Yadunund changed the title Sync main with rolling Fix eigen not found when building rpm on main May 26, 2023
@Yadunund Yadunund merged commit 836779a into main May 26, 2023
@Yadunund Yadunund deleted the rolling branch May 26, 2023 07:36
@Yadunund Yadunund restored the rolling branch June 1, 2023 16:58
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.

4 participants