author | wenzelm |
Fri, 04 Jun 2021 21:46:14 +0200 | |
changeset 73799 | 1262fefabc9a |
parent 73798 | 1ca35197108f |
child 73800 | 4addb9707200 |
--- a/src/Pure/Thy/thy_info.ML Fri Jun 04 21:36:42 2021 +0200 +++ b/src/Pure/Thy/thy_info.ML Fri Jun 04 21:46:14 2021 +0200 @@ -254,7 +254,6 @@ {name = "present", sequential = sequential_presentation (Options.default ())} (fn result => Exn.capture (result_present result) ()); - (* FIXME more precise commit order (!?) *) val results3 = futures |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());