src/Pure/System/host.scala
Wed, 14 Feb 2024 11:08:05 +0100 wenzelm clarified signature;
Thu, 26 Oct 2023 12:36:19 +0200 wenzelm proper support for SSH;
Thu, 26 Oct 2023 12:27:10 +0200 wenzelm tuned signature;
Wed, 18 Oct 2023 19:49:08 +0200 Fabian Huch added initial version of benchmark module, e.g., to compare performance of different hosts;
Wed, 18 Oct 2023 19:26:37 +0200 Fabian Huch generalized node infos: allow addressing of numa node segments via relative cpus;
Wed, 18 Oct 2023 19:05:06 +0200 Fabian Huch add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Wed, 18 Oct 2023 18:53:26 +0200 Fabian Huch added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Sat, 22 Jul 2023 16:01:46 +0200 wenzelm more flexible Build.Engine.process_options: e.g. to manipulate "process_policy" for ML process;
Tue, 18 Jul 2023 19:51:12 +0200 wenzelm renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
Sun, 16 Jul 2023 11:29:23 +0200 wenzelm more informative trace;
Sat, 08 Jul 2023 13:13:10 +0200 wenzelm clarified signature;
Wed, 21 Jun 2023 14:27:51 +0200 wenzelm clarified signature: more explicit class SQL.Data;
Sat, 17 Jun 2023 15:58:41 +0200 wenzelm separate host.db for independent db.transaction_lock;
Mon, 06 Mar 2023 21:12:47 +0100 wenzelm clarified signature: reduce boilerplate;
Mon, 06 Mar 2023 19:18:53 +0100 wenzelm tuned signature;
Mon, 06 Mar 2023 19:13:27 +0100 wenzelm tuned structure;
Mon, 06 Mar 2023 19:09:17 +0100 wenzelm clarified signature;
Mon, 06 Mar 2023 18:58:48 +0100 wenzelm clarified signature;
Mon, 06 Mar 2023 15:56:28 +0100 wenzelm tuned whitespace and braces;
Mon, 06 Mar 2023 15:38:50 +0100 wenzelm tuned signature: reduce boilerplate;
Sun, 05 Mar 2023 19:33:01 +0100 wenzelm tuned output;
Sun, 05 Mar 2023 19:21:07 +0100 wenzelm clarified database content: store actual value instead of index;
Thu, 02 Mar 2023 16:09:22 +0100 wenzelm clarified names;
Thu, 02 Mar 2023 15:04:24 +0100 wenzelm tuned comments;
Thu, 02 Mar 2023 14:58:59 +0100 wenzelm clarified modules;
Thu, 02 Mar 2023 14:41:21 +0100 wenzelm clarified modules;
Thu, 02 Mar 2023 14:22:17 +0100 wenzelm clarified modules;
less more (0) tip