jupyterhub / nbgitpuller

Jupyter server extension to sync a git repository one-way to a local path
https://nbgitpuller.readthedocs.io
BSD 3-Clause "New" or "Revised" License
210 stars 86 forks source link

Add binder-badge bot #259

Open manics opened 2 years ago

manics commented 2 years ago

This is an optional add-on to https://github.com/jupyterhub/nbgitpuller/pull/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. https://github.com/manics/nbgitpuller/pull/2

consideRatio commented 1 year ago

@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.