mirror/notebook
2
0
Fork 0
mirror of https://github.com/jupyter/notebook.git synced 2025-01-12 11:45:38 +08:00
Code Issues Packages Projects Releases Wiki Activity

Make buffer time between last modified on disk and last modified on last save configurable

Browse Source
This commit is contained in:
Grant Nestor 2018-01-27 18:14:06 -08:00
parent b96d75846d
commit c2701a8fb0
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
notebook/static/notebook/js/notebook.js
View File

@ -2738,10 +2738,11 @@ define([
return this.contents.get(this.notebook_path, {content: false}).then(
function (data) {
var last_modified = new Date(data.last_modified);
var difference_buffer = that.config.data['last_modified_buffer'] || 500; // 500 ms
// 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.
if ((last_modified.getTime() - that.last_modified.getTime()) > difference_buffer) {
console.warn("Last saving was done on `"+that.last_modified+"`("+that._last_modified+"), "+
"while the current file seem to have been saved on `"+data.last_modified+"`");
if (that._changed_on_disk_dialog !== null) {