-
Notifications
You must be signed in to change notification settings - Fork 5.1k
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
Make buffer time between last modified on disk and last modified on last save configurable #3273
Conversation
…ast save configurable
I'm trying to think of a better word than 'buffer', because that suggests a temporary storage area for data. Maybe Also, I might make the config option in seconds rather than milliseconds; I think we generally try to keep intervals in seconds throughout our API for consistency (cc @minrk ) |
// We want to check last_modified (disk) > that.last_modified (our last save) | ||
// In some cases the filesystem reports an inconsistent time, | ||
// so we allow 0.5 seconds difference before complaining. | ||
if ((last_modified.getTime() - that.last_modified.getTime()) > 500) { // 500 ms | ||
// so we allow 0.5 seconds (configurable in nbconfig/notebook.json as `last_modified_buffer`) difference before complaining. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Don't forget to update the name in the comment too.
Adding the line |
Is there any plan to have this property configurable in Jupyter lab as well? |
@ckbhatt I opened jupyterlab/jupyterlab#8556 to track the feature in JupyterLab. |
Suggested by #484 (comment)
This will look in
notebook.json
in~/.jupyter/nbconfig/notebook.json
for alast_modified_buffer
value. For example:Can anyone think of better name than
last_modified_buffer
?