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

Add binder-badge bot #259

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Add binder-badge bot #259

wants to merge 1 commit into from

Conversation

manics
Copy link
Member

@manics manics commented Mar 17, 2022

This is an optional add-on to #258

This will update a PR description (so avoids the noise of a new comment) with a mybinder.org badge that builds the PR on mybinder.org, and redirects to nbgitpuller to clone a repo, for now I've picked https://github.com/jupyterhub/nbgitpuller

See e.g. manics#2

@manics manics added the ci label Mar 17, 2022
@@ -0,0 +1,18 @@
name: binder-badge
Copy link
Member

Choose a reason for hiding this comment

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

Can you add an inline comment to clarify with a sentence what this workflow does and for what reason?

@consideRatio
Copy link
Member

@manics I was about to go for a merge here, looking through PRs to get reviewed and/or merged before a release - but I see that this is referencing 1.0.0 of the action, while I know a 2.0.0 version is out among other things.

If you refresh this, feel free to either self-merge of ping me for a review and I'll quickly go for a review -> merge.

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

Successfully merging this pull request may close these issues.

2 participants