added a check for existence of a temporary file before removing it
authorclasohm
Mon, 10 Jan 1994 16:58:32 +0100
changeset 221 3886a320c5bc
parent 220 e50ea2471e06
child 222 5eb3020f7a03
added a check for existence of a temporary file before removing it
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;