From d60426e9a644b9c521d8cbf406d88f1f9ba36080 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Fri, 13 Apr 2012 10:04:25 -0500 Subject: [PATCH] the autosave file might be deleted by the user after it is created the first time but before the file is actually saved. guard against that. closes PR 12698 original commit: 35e818ae50eea159f10c996c3475198bc321c662 --- collects/framework/private/editor.rkt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/collects/framework/private/editor.rkt b/collects/framework/private/editor.rkt index 2e800662..690c6bb5 100644 --- a/collects/framework/private/editor.rkt +++ b/collects/framework/private/editor.rkt @@ -598,7 +598,8 @@ (when (is-a? this text%) (send this set-file-format orig-format)) (when old-auto-name - (delete-file old-auto-name)) + (when (file-exists? old-auto-name) + (delete-file old-auto-name))) (set! auto-saved-name auto-name) (set! auto-save-out-of-date? #f) auto-name))]