# HG changeset patch
# User wenzelm
# Date 1626553047 -7200
# Node ID ec3249dd63dd908ea321c439d7e20c8abdf386f5
# Parent  d6ae3a7d9cb0193c7ecb96b0b647cd9665bf01da
more portable across history;

diff -r d6ae3a7d9cb0 -r ec3249dd63dd src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Jul 17 22:12:06 2021 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Jul 17 22:17:27 2021 +0200
@@ -564,7 +564,7 @@
 
       execute("bin/isabelle", "components -I")
       execute("bin/isabelle", "components -a", echo = true)
-      execute("Admin/build", "jars_fresh")
+      execute("bin/isabelle", "jedit -bf")
     }
 
     val rev_id = self_hg.id(rev)