Sun, 19 Nov 2023 12:51:47 +0100 unused (see also 004b39bf06a5);
wenzelm [Sun, 19 Nov 2023 12:51:47 +0100] rev 78992
unused (see also 004b39bf06a5);
Sun, 19 Nov 2023 12:46:41 +0100 clarified signature and modules: more explicit Build_Log.History;
wenzelm [Sun, 19 Nov 2023 12:46:41 +0100] rev 78991
clarified signature and modules: more explicit Build_Log.History;
Sat, 18 Nov 2023 21:14:34 +0100 tuned: avoid recursion;
wenzelm [Sat, 18 Nov 2023 21:14:34 +0100] rev 78990
tuned: avoid recursion;
Sat, 18 Nov 2023 20:51:44 +0100 tuned;
wenzelm [Sat, 18 Nov 2023 20:51:44 +0100] rev 78989
tuned;
Sat, 18 Nov 2023 19:31:22 +0100 avoid duplicate data;
wenzelm [Sat, 18 Nov 2023 19:31:22 +0100] rev 78988
avoid duplicate data;
Sat, 18 Nov 2023 19:14:59 +0100 output more data;
wenzelm [Sat, 18 Nov 2023 19:14:59 +0100] rev 78987
output more data;
Sat, 18 Nov 2023 18:52:34 +0100 tuned whitespace;
wenzelm [Sat, 18 Nov 2023 18:52:34 +0100] rev 78986
tuned whitespace;
Sat, 18 Nov 2023 16:58:14 +0100 clarified Log_File.cache: reuse existing Store.cache / Build_Log.Store.cache;
wenzelm [Sat, 18 Nov 2023 16:58:14 +0100] rev 78985
clarified Log_File.cache: reuse existing Store.cache / Build_Log.Store.cache;
Sat, 18 Nov 2023 15:44:46 +0100 proper ml_statistics (amending aeb511a520f4);
wenzelm [Sat, 18 Nov 2023 15:44:46 +0100] rev 78984
proper ml_statistics (amending aeb511a520f4);
Fri, 17 Nov 2023 10:11:15 +0100 unify error messages;
Fabian Huch <huch@in.tum.de> [Fri, 17 Nov 2023 10:11:15 +0100] rev 78983
unify error messages;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 tip