# HG changeset patch # User clasohm # Date 758217512 -3600 # Node ID 3886a320c5bcadde9f45a19db2f096ea34101ade # Parent e50ea2471e068d96d647f6ea894c7db49ce32530 added a check for existence of a temporary file before removing it diff -r e50ea2471e06 -r 3886a320c5bc src/Pure/Thy/read.ML --- a/src/Pure/Thy/read.ML Mon Jan 10 16:57:31 1994 +0100 +++ b/src/Pure/Thy/read.ML Mon Jan 10 16:58:32 1994 +0100 @@ -274,8 +274,10 @@ (*Mark theories that have to be reloaded.*) mark_children thy_name; - if !delete_tmpfiles then delete_file (out_name thyl) - else () + if not (!delete_tmpfiles) orelse (thy_file = "") + orelse thy_uptodate + then () + else delete_file (out_name thyl) ) end;