Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

New release with missing headers #15272

Closed
zerothi opened this issue May 26, 2023 · 3 comments
Closed

New release with missing headers #15272

zerothi opened this issue May 26, 2023 · 3 comments

Comments

@zerothi
Copy link

zerothi commented May 26, 2023

Would it be possible to create a new release with 4292ae6 since the missing headers causes problems on my build.

Thanks!

@drwells
Copy link
Member

drwells commented May 26, 2023

We're getting ready to release deal.II 9.5 in the next month or so - will that work for you?

@zerothi
Copy link
Author

zerothi commented May 26, 2023

Yeah, that would be fine. :) thanks

@drwells
Copy link
Member

drwells commented May 27, 2023

This is already underway so I'm going to close this issue - we'll have 9.5 done in the next month or so.

@drwells drwells closed this as completed May 27, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants