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

nicer infinity #38

Closed
wants to merge 1 commit into from
Closed

Conversation

havogt
Copy link
Owner

@havogt havogt commented Aug 18, 2023

Description

Describe the content of the PR and links to related issues, bugs of features.

Requirements

Before submitting this PR, please make sure:

  • You have run the code checks, tests and documentation build successfully
  • All fixes and all new functionality are tested and documentation is up to date
  • You looked at the review checklist

Additionally, if this PR contains code authored by new contributors:

  • All the authors are covered by a valid contributor assignment agreement,
    signed by the employer if needed, provided to ETH Zurich
  • The names of all the new contributors have been added to an updated
    version of the AUTHORS.rst file included in the PR

@havogt havogt closed this Oct 1, 2024
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.

1 participant