# HG changeset patch
# User wenzelm
# Date 1689704097 -7200
# Node ID ea5adf7acc2d9cd78fe00c041be8d158c1bb4792
# Parent  c8df7abb8707165ae973110011770a3541e7922a
support for management of build cluster;

diff -r c8df7abb8707 -r ea5adf7acc2d etc/build.props
--- a/etc/build.props	Tue Jul 18 19:41:56 2023 +0200
+++ b/etc/build.props	Tue Jul 18 20:14:57 2023 +0200
@@ -189,6 +189,7 @@
   src/Pure/Thy/thy_header.scala \
   src/Pure/Thy/thy_syntax.scala \
   src/Pure/Tools/build.scala \
+  src/Pure/Tools/build_cluster.scala \
   src/Pure/Tools/build_job.scala \
   src/Pure/Tools/build_process.scala \
   src/Pure/Tools/check_keywords.scala \
diff -r c8df7abb8707 -r ea5adf7acc2d src/Pure/Tools/build_cluster.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/build_cluster.scala	Tue Jul 18 20:14:57 2023 +0200
@@ -0,0 +1,12 @@
+/*  Title:      Pure/Tools/build_cluster.scala
+    Author:     Makarius
+
+Management of build cluster: independent ssh hosts with access to shared
+PostgreSQL server.
+*/
+
+package isabelle
+
+
+object Build_Cluster {
+}