[BLUEJ-1260] Allow tolerance of file change times
We currently detect if the file modification time on disk is more recent than we think we last issued the save. But due to network lag and time sync issues, it can be that the legitimate last disk modification time ends up a few seconds after when we issued the last save. In this case, users get an annoying dialog about editing outside BlueJ and wanting to reload. We can help them out by adding a tolerance (15 seconds? 30?) since last save where we no longer warn users about this issue if the datetimes do not match.
Issue metadata
- Issue type: Bug
- Priority: Medium
- Fix versions: 4.2.1