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

Page-level over-riding of launch button functionality #587

Open
choldgraf opened this issue Jul 13, 2022 · 0 comments
Open

Page-level over-riding of launch button functionality #587

choldgraf opened this issue Jul 13, 2022 · 0 comments
Labels
enhancement New feature or request

Comments

@choldgraf
Copy link
Member

Context

Currently, our launch buttons are configured at the documentation-level. The GitHub repository etc are defined in conf.py and then used in each page.

However, there are some cases where users might want to specify per-page Binder configuration. For example, if a book has notebooks that require many different packages / languages / etc, the author might prefer to define a Binder environment for each in a different branch (or, multiple repositories), and then create different Binder links on each. (cc @acocac)

Proposal

We could make it possible to define page-level over-rides for launch buttons. For example, here might be two page-level over-rides, and each would over-ride the corresponding fields in the docs-level launch: configuration.

launch:
  repository_url: https://github.com/foo/bar
  branch: foo

and on another page:

launch:
  repository_url: https://github.com/foo/bar
  branch: bar

It might be tricky to get the UX right on this, because people probably won't want to duplicate their content, only the environment needed to run that content. So I think this might also depend on:

Tasks and updates

No response

@choldgraf choldgraf added the enhancement New feature or request label Jul 13, 2022
@choldgraf choldgraf changed the title Allow page-level over-riding of launch button functionality Page-level over-riding of launch button functionality Jul 13, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

1 participant