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.

Sign up for GitHub

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

Jump to bottom

fix: update ninja build resource #15378

Merged

masterleinad merged 1 commit into dealii:master from emmanuel-ferdman:wip

Jun 19, 2023

Contributor

emmanuel-ferdman commented Jun 18, 2023

PR Summary:
The PR contains a fix to the broken hyperlink leading to ninja build resource.

drwells approved these changes

View reviewed changes

Member

drwells commented Jun 18, 2023

Thanks!

drwells added the Documentation label

tamiko approved these changes

View reviewed changes


          fix: update ninja build resource

a996eec

masterleinad approved these changes

View reviewed changes

masterleinad merged commit e220f9b into dealii:master

11 of 14 checks passed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment