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

fix Issue [#2178] and Issue [#2167] #2187

Closed
wants to merge 3 commits into from
Closed

fix Issue [#2178] and Issue [#2167] #2187

wants to merge 3 commits into from

Conversation

Larpoux
Copy link
Contributor

@Larpoux Larpoux commented Jul 4, 2024

Changes

fix Issue [#2178] and Issue [#2167].

Close #2167 , Close #2178 (use this format to let github understand it)

Checklist

  • An issue to be fixed by this PR is listed above.
  • New tests are added to ensure new features are working. Please refer to this page to see how to add a test.
  • ./frb_internal precommit --mode slow (or fast) is run (it internal runs code generator, does auto formatting, etc).
  • If this PR adds/changes features, documentations (in the ./website folder) are updated.
  • CI is passing. Please refer to this page to see how to solve a failed CI.

Remark for PR creator

  • ./frb_internal --help shows utilities for development.
  • If fzyzcjy does not reply for a few days, maybe he just did not see it, so please ping him.

I hope that this PR is OK. I did my best 😃

Copy link
Owner

@fzyzcjy fzyzcjy left a comment

Choose a reason for hiding this comment

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

Good job! Only a few nits

@fzyzcjy
Copy link
Owner

fzyzcjy commented Jul 4, 2024

Other things to do before merging

  • Make CI green (just run the commands mentioned before and it should be automatically ok)

@Canardoux Canardoux closed this by deleting the head repository Jul 5, 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
3 participants