proper order of operations: archive before purge;
authorwenzelm
Sun, 02 Feb 2025 21:53:08 +0100
changeset 82055 8fd693bb01c5
parent 82054 cddcc84309a5
child 82056 361fbb3e21c8
proper order of operations: archive before purge;
src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Sun Feb 02 17:25:12 2025 +0100
+++ b/src/Pure/Admin/build_release.scala	Sun Feb 02 21:53:08 2025 +0100
@@ -510,6 +510,13 @@
           database_dir.dir.dir.file.delete  // "$FIND_FACTS_HOME_USER"
         }
 
+        if (build_library) {
+          progress.echo_warning(
+            "Creating library archive " + context.isabelle_library_archive + " ...")
+          execute_tar(context.dist_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
+            " " + Bash.string(context.dist_name + "/browser_info"))
+        }
+
         if (!include_library) other_isabelle_purge("browser_info")
       }
 
@@ -527,12 +534,6 @@
         """find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""")
       execute_tar(context.dist_dir, "-czf " +
         File.bash_path(context.isabelle_archive) + " " + Bash.string(context.dist_name))
-
-      if (build_library) {
-        progress.echo_warning("Creating library archive " + context.isabelle_library_archive + " ...")
-        execute_tar(context.dist_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
-          " " + Bash.string(context.dist_name + "/browser_info"))
-      }
     }
   }