Thu, 16 Mar 2023 15:55:49 +0100 proper vacuum of session_info tables: only once per build process;
wenzelm [Thu, 16 Mar 2023 15:55:49 +0100] rev 77678
proper vacuum of session_info tables: only once per build process;
Thu, 16 Mar 2023 15:46:10 +0100 tuned signature;
wenzelm [Thu, 16 Mar 2023 15:46:10 +0100] rev 77677
tuned signature;
Thu, 16 Mar 2023 15:38:32 +0100 more thorough database checks;
wenzelm [Thu, 16 Mar 2023 15:38:32 +0100] rev 77676
more thorough database checks;
Thu, 16 Mar 2023 15:16:17 +0100 more thorough treatment of build prefs, guarded by system option "build_through": avoid accidental rebuild of HOL etc.;
wenzelm [Thu, 16 Mar 2023 15:16:17 +0100] rev 77675
more thorough treatment of build prefs, guarded by system option "build_through": avoid accidental rebuild of HOL etc.;
Thu, 16 Mar 2023 13:18:25 +0100 clarified build options;
wenzelm [Thu, 16 Mar 2023 13:18:25 +0100] rev 77674
clarified build options;
Thu, 16 Mar 2023 11:44:07 +0100 clarified ML option vs. Scala option (see also caa182bdab7a);
wenzelm [Thu, 16 Mar 2023 11:44:07 +0100] rev 77673
clarified ML option vs. Scala option (see also caa182bdab7a);
Thu, 16 Mar 2023 13:37:49 +0100 merge conflict
nipkow [Thu, 16 Mar 2023 13:37:49 +0100] rev 77672
merge conflict
Thu, 16 Mar 2023 08:30:00 +0100 unified function update and map update syntaxes
nipkow [Thu, 16 Mar 2023 08:30:00 +0100] rev 77671
unified function update and map update syntaxes
Wed, 15 Mar 2023 15:28:44 +0100 removed accidental junk
blanchet [Wed, 15 Mar 2023 15:28:44 +0100] rev 77670
removed accidental junk
Wed, 15 Mar 2023 13:01:57 +0100 map update syntax
nipkow [Wed, 15 Mar 2023 13:01:57 +0100] rev 77669
map update syntax
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 tip