# HG changeset patch
# User paulson
# Date 1530830237 -3600
# Node ID 57b9d993cc987e41f3898a64551a5b40d92a9205
# Parent  90381a0f54740c5e1417a3ca2f5b2777984f0315# Parent  5b05ede597b8d0004df01450f1b0feff667f4ada
merged

diff -r 5b05ede597b8 -r 57b9d993cc98 Admin/Release/CHECKLIST
--- 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'
diff -r 5b05ede597b8 -r 57b9d993cc98 src/Pure/Concurrent/lazy.ML
--- 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) ());