# HG changeset patch
# User wenzelm
# Date 1646585547 -3600
# Node ID 8945d691ecf2310bcd1a8fc22fc41cba2cc638df
# Parent  bbbee54b119856583bc9ca251e76499c5b92a664
more compact result;

diff -r bbbee54b1198 -r 8945d691ecf2 src/Pure/Admin/build_vscodium.scala
--- a/src/Pure/Admin/build_vscodium.scala	Sun Mar 06 17:45:47 2022 +0100
+++ b/src/Pure/Admin/build_vscodium.scala	Sun Mar 06 17:52:27 2022 +0100
@@ -324,6 +324,8 @@
       })
     }
 
+    Isabelle_System.bash("gzip *.patch", cwd = patches_dir.file).check
+
 
     /* settings */