Use now fixed DirectoryMonitor.ignore property in webide

This commit is contained in:
Kristóf Tóth 2018-03-20 11:39:37 +01:00
parent 08693d3ba2
commit b1f4842dc7

View File

@ -102,7 +102,7 @@ class SourceCodeEventHandler(TriggerlessEventHandler):
return data
def write(self, data):
self.monitor.eventhandler.ignore = 1
self.monitor.ignore = self.monitor.ignore + 1
try: self.filemanager.file_contents = data['content']
except Exception: log.exception('Error writing file!')
del data['content']