avoid change of existing file, notably rebuild via ghc_stack;
authorwenzelm
Mon, 30 Aug 2021 21:18:49 +0200
changeset 74215 7515abfe18cf
parent 74214 e16ac8907148
child 74216 a308ed696b58
avoid change of existing file, notably rebuild via ghc_stack;
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)
           }
         }