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.

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

feat: merge polls in one #1

Merged
merged 4 commits into from
Dec 4, 2023
Merged

feat: merge polls in one #1

merged 4 commits into from
Dec 4, 2023

Conversation

NoeTerrier
Copy link
Contributor

Merge polls in one

@NoeTerrier NoeTerrier self-assigned this Nov 23, 2023
Thechi2000
Thechi2000 requested changes Nov 27, 2023
View reviewed changes
NoeTerrier and others added 2 commits November 29, 2023 09:13
@NoeTerrier @Thechi2000
Update src/commands.rs
c025d84 
Co-authored-by: Ludovic Mermod <ludovic.mermod@epfl.ch>
@NoeTerrier
fix: small correction in /poll command
532443f
@NoeTerrier NoeTerrier requested a review from Thechi2000 December 4, 2023 09:06
Thechi2000
Thechi2000 approved these changes Dec 4, 2023
View reviewed changes
Copy link
Contributor

@Thechi2000 Thechi2000 left a comment

Choose a reason for hiding this comment

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

Looks good to me !
Tested locally, works perfectly well.

@Thechi2000 Thechi2000 merged commit 816ea00 into main Dec 4, 2023
@NoeTerrier NoeTerrier deleted the merge-polls-in-one branch April 19, 2024 16:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Thechi2000 Thechi2000 Thechi2000 approved these changes

@SidonieBouthors SidonieBouthors Awaiting requested review from SidonieBouthors

Assignees

@NoeTerrier NoeTerrier

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@NoeTerrier @Thechi2000