Skip to content

Conversation

arnavkohli
Copy link
Collaborator

@arnavkohli arnavkohli commented Mar 14, 2020

Removed an unneeded provision check and corrected a typo.

Fixes #489

@timabbott
Copy link
Member

@arnavkohli can you clean up the commit history here?

Check out our GitHub guide and commit guidelines for more details.

@arnavkohli
Copy link
Collaborator Author

arnavkohli commented Mar 25, 2020

@timabbott done! Let me know if any other changes are required.

@PIG208
Copy link
Member

PIG208 commented Jun 14, 2021

This should be ready to merge if we clean up the commit history

@zulipbot
Copy link
Member

Heads up @arnavkohli, we just merged some commits that conflict with the changes your made in this pull request! You can review this repository's recent commits to see where the conflicts occur. Please rebase your feature branch against the upstream/main branch and resolve your pull request's merge conflicts accordingly.

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

Successfully merging this pull request may close these issues.

bots: Fix error handling for bot not found.
4 participants