changeset 62891 | 7a11ea5c9626 |
parent 62879 | 4764473c9b8d |
--- a/src/Pure/System/windows/bash.ML Wed Apr 06 16:51:52 2016 +0200 +++ b/src/Pure/System/windows/bash.ML Wed Apr 06 17:16:30 2016 +0200 @@ -12,7 +12,7 @@ structure Bash: BASH = struct -val process = uninterruptible (fn restore_attributes => fn script => +val process = Multithreading.uninterruptible (fn restore_attributes => fn script => let datatype result = Wait | Signal | Result of int; val result = Synchronized.var "bash_result" Wait;