wenzelm [Sat, 18 Nov 2023 18:52:34 +0100] rev 78986
tuned whitespace;
wenzelm [Sat, 18 Nov 2023 16:58:14 +0100] rev 78985
clarified Log_File.cache: reuse existing Store.cache / Build_Log.Store.cache;
wenzelm [Sat, 18 Nov 2023 15:44:46 +0100] rev 78984
proper ml_statistics (amending aeb511a520f4);
Fabian Huch <huch@in.tum.de> [Fri, 17 Nov 2023 10:11:15 +0100] rev 78983
unify error messages;
Fabian Huch <huch@in.tum.de> [Fri, 17 Nov 2023 09:38:15 +0100] rev 78982
add file information to toml parse context and error messages;
Fabian Huch <huch@in.tum.de> [Fri, 17 Nov 2023 09:23:28 +0100] rev 78981
add position information to toml parser and error messages;
Fabian Huch <huch@in.tum.de> [Thu, 16 Nov 2023 15:36:34 +0100] rev 78980
properly concatenate toml files: regular toml rules still apply (e.g., inline values may not be changed), but values defined in one file may be updated in another;
Fabian Huch <huch@in.tum.de> [Thu, 16 Nov 2023 15:23:41 +0100] rev 78979
allow re-defining keys in toml object (already checked during parse time);
Fabian Huch <huch@in.tum.de> [Thu, 16 Nov 2023 15:19:24 +0100] rev 78978
clarified toString for toml objects;
nipkow [Thu, 16 Nov 2023 14:33:45 +0100] rev 78977
tuned