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 a reload button to the editor #50

Closed
JamesWrigley opened this issue Jul 11, 2023 · 1 comment
Closed

Add a reload button to the editor #50

JamesWrigley opened this issue Jul 11, 2023 · 1 comment
Labels
enhancement New feature or request GUI For GUI-related things

Comments

@JamesWrigley
Copy link
Member

The context file can be modified simultaneously by multiple people either through the GUIs or through e.g. Jupyterhub or a terminal editor, and when this happens there's a danger of a user with an old version of the context file accidentally saving the old version. Ignoring the can of worms around merge conflicts, we should at least add a reload button to the editor and notify the user that the file has changed. Partially implemented in e119354.

@JamesWrigley JamesWrigley added enhancement New feature or request GUI For GUI-related things labels Jul 11, 2023
@JamesWrigley
Copy link
Member Author

Closing because this was merged in #119.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request GUI For GUI-related things
Projects
None yet
Development

No branches or pull requests

1 participant