diff options
Diffstat (limited to 'ide/fileOps.ml')
| -rw-r--r-- | ide/fileOps.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/fileOps.ml b/ide/fileOps.ml index 03b3fcd4e..b8e1861ef 100644 --- a/ide/fileOps.ml +++ b/ide/fileOps.ml @@ -87,7 +87,7 @@ object(self) flash_info "Could not overwrite file" | _ -> Minilib.log "Auto revert set to false"; - prefs.Preferences.global_auto_revert <- false; + Preferences.global_auto_revert#set false; revert_timer.kill () method save f = |