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

See gh-484

Author: takluyver

notebook/static/notebook/js/notebook.js

@@ -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) {