# HG changeset patch
# User wenzelm
# Date 1630351129 -7200
# Node ID 7515abfe18cf7e61db0cb198e24f72c8cc4629cd
# Parent  e16ac8907148a66d5188c9d8909a007702537029
avoid change of existing file, notably rebuild via ghc_stack;

diff -r e16ac8907148 -r 7515abfe18cf src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon Aug 30 21:10:13 2021 +0200
+++ b/src/Pure/Thy/export.scala	Mon Aug 30 21:18:49 2021 +0200
@@ -376,7 +376,8 @@
 
             progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
             Isabelle_System.make_directory(path.dir)
-            Bytes.write(path, entry.uncompressed)
+            val bytes = entry.uncompressed
+            if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes)
             File.set_executable(path, entry.executable)
           }
         }