Skip to content

add bors#303

Merged
japaric merged 1 commit intomainfrom
bors
Dec 15, 2020
Merged

add bors#303
japaric merged 1 commit intomainfrom
bors

Conversation

@japaric
Copy link
Copy Markdown
Member

@japaric japaric commented Dec 15, 2020

No description provided.

@japaric
Copy link
Copy Markdown
Member Author

japaric commented Dec 15, 2020

bors ping

@bors
Copy link
Copy Markdown
Contributor

bors Bot commented Dec 15, 2020

pong

@japaric
Copy link
Copy Markdown
Member Author

japaric commented Dec 15, 2020

bors r+

bors Bot added a commit that referenced this pull request Dec 15, 2020
303: add bors r=japaric a=japaric



Co-authored-by: Jorge Aparicio <jorge.aparicio@ferrous-systems.com>
@japaric japaric merged commit 2039cb5 into main Dec 15, 2020
@japaric japaric deleted the bors branch December 15, 2020 10:42
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