# HG changeset patch
# User wenzelm
# Date 1621276662 -7200
# Node ID 7c2f7688a5a86470027c63db0163a8f1cc7db86e
# Parent  d4c7b88f56a0d29cb98051b91aec55fd59c41dfb
redundant: tmp_dir is purged anyway;

diff -r d4c7b88f56a0 -r 7c2f7688a5a8 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Mon May 17 20:32:52 2021 +0200
+++ b/src/Pure/Thy/document_build.scala	Mon May 17 20:37:42 2021 +0200
@@ -230,10 +230,7 @@
         old_doc <- db_context.input_database(session)(read_document(_, _, directory.doc.name))
         if old_doc.sources == directory.sources
       }
-      yield {
-        old_doc.write(directory.doc_dir)
-        old_doc
-      }
+      yield old_doc
   }
 
   sealed case class Content(path: Path, bytes: Bytes)