src/Pure/Tools/build_process.scala
Wed, 01 Mar 2023 13:55:49 +0100 wenzelm tuned signature;
Wed, 01 Mar 2023 13:52:11 +0100 wenzelm avoid premature Properties.uncompress: allow blob to be stored in another database;
Wed, 01 Mar 2023 13:30:35 +0100 wenzelm more robust: synchronized access to database;
less more (0) -30 -10 -3 tip