--- a/Admin/Release/CHECKLIST Thu Jul 05 23:37:00 2018 +0100
+++ b/Admin/Release/CHECKLIST Thu Jul 05 23:37:17 2018 +0100
@@ -17,6 +17,9 @@
- test "#!/usr/bin/env isabelle_scala_script";
+- test Windows 10 subsystem for Linux:
+ https://docs.microsoft.com/en-us/windows/wsl/install-win10
+
- check sources:
isabelle check_sources '~~' '$AFP_BASE'
isabelle imports -M -a -d '~~/src/Benchmarks'
--- a/src/Pure/Concurrent/lazy.ML Thu Jul 05 23:37:00 2018 +0100
+++ b/src/Pure/Concurrent/lazy.ML Thu Jul 05 23:37:17 2018 +0100
@@ -100,9 +100,9 @@
(*semantic race: some other threads might see the same
interrupt, until there is a fresh start*)
val _ =
- if Exn.is_interrupt_exn res then
- Synchronized.change var (fn _ => Expr (name, e))
- else ();
+ if Exn.is_interrupt_exn res
+ then Synchronized.change var (fn _ => Expr (name, e))
+ else Synchronized.change var (fn _ => Result (Future.value_result res));
in res end
| NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
end) ());