Skip to content

Merge to insiders (again)#13269

Closed
sean-mcmanus wants to merge 1 commit intoinsidersfrom
main
Closed

Merge to insiders (again)#13269
sean-mcmanus wants to merge 1 commit intoinsidersfrom
main

Conversation

@sean-mcmanus
Copy link
Contributor

  • convert the time budget integer to a real number.

  • update the changes' log

* convert the time budget integer to a real number.

* update the changes' log
@sean-mcmanus sean-mcmanus requested a review from a team as a code owner February 11, 2025 01:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

Status: Pull Request

Development

Successfully merging this pull request may close these issues.

2 participants