Allow 0.5 seconds difference in file timestamps before warning of conflicting changes

See gh-484
This commit is contained in:
Thomas Kluyver 2017-07-27 13:24:49 +01:00
parent 8af8b0eb9b
commit fd34dd2052

View File

@ -2721,7 +2721,10 @@ define([
return this.contents.get(this.notebook_path, {content: false}).then(
function (data) {
var last_modified = new Date(data.last_modified);
if (last_modified > that.last_modified) {
// 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
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) {